Commit 7a7afe6a authored by Andrei Paskevich's avatar Andrei Paskevich

tptp typing (cont.)

parent f167fabd
...@@ -50,6 +50,7 @@ exception FmlaExpected ...@@ -50,6 +50,7 @@ exception FmlaExpected
exception TVarExpected exception TVarExpected
exception VarExpected exception VarExpected
exception InvalidDummy exception InvalidDummy
exception BadArity
let () = Exn_printer.register (fun fmt e -> match e with let () = Exn_printer.register (fun fmt e -> match e with
| Message s -> fprintf fmt "%s" s | Message s -> fprintf fmt "%s" s
...@@ -60,14 +61,15 @@ let () = Exn_printer.register (fun fmt e -> match e with ...@@ -60,14 +61,15 @@ let () = Exn_printer.register (fun fmt e -> match e with
| TVarExpected -> fprintf fmt "type variable expected" | TVarExpected -> fprintf fmt "type variable expected"
| VarExpected -> fprintf fmt "term variable expected" | VarExpected -> fprintf fmt "term variable expected"
| InvalidDummy -> fprintf fmt "invalid type placeholder" | InvalidDummy -> fprintf fmt "invalid type placeholder"
| BadArity -> fprintf fmt "bad arity"
| _ -> raise e) | _ -> raise e)
type symbol = type symbol =
| STVar of tvsymbol | STVar of tvsymbol
| SVar of vsymbol | SVar of vsymbol
| SType of tysymbol | SType of tysymbol
| SFunc of lsymbol | SFunc of tvsymbol list * lsymbol
| SPred of lsymbol | SPred of tvsymbol list * lsymbol
| SletF of tvsymbol list * vsymbol list * term | SletF of tvsymbol list * vsymbol list * term
| SletP of tvsymbol list * vsymbol list * term | SletP of tvsymbol list * vsymbol list * term
...@@ -111,7 +113,7 @@ let find_fs ~loc impl env s args = ...@@ -111,7 +113,7 @@ let find_fs ~loc impl env s args =
try Mstr.find s env with Not_found -> try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found -> try Hashtbl.find impl s with Not_found ->
let args = List.map (fun _ -> ty_univ) args in let args = List.map (fun _ -> ty_univ) args in
let fs = SFunc (create_fsymbol (id_user s loc) args ty_univ) in let fs = SFunc ([], create_fsymbol (id_user s loc) args ty_univ) in
Hashtbl.add impl s fs; Hashtbl.add impl s fs;
fs fs
...@@ -119,18 +121,18 @@ let find_ps ~loc impl env s args = ...@@ -119,18 +121,18 @@ let find_ps ~loc impl env s args =
try Mstr.find s env with Not_found -> try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found -> try Hashtbl.find impl s with Not_found ->
let args = List.map (fun _ -> ty_univ) args in let args = List.map (fun _ -> ty_univ) args in
let ps = SPred (create_psymbol (id_user s loc) args) in let ps = SPred ([], create_psymbol (id_user s loc) args) in
Hashtbl.add impl s ps; Hashtbl.add impl s ps;
ps ps
let rec ty defenv impl env { e_loc = loc; e_node = n } = match n with let rec ty defenv impl env { e_loc = loc; e_node = n } = match n with
| Eapp (aw,args) -> | Eapp (aw,al) ->
let ts = match find_ts ~loc impl env aw args with let ts = match find_ts ~loc impl env aw al with
| SType ts -> ts | SType ts -> ts
| _ -> error ~loc TypeExpected in | _ -> error ~loc TypeExpected in
let tys = List.map (ty defenv impl env) args in let tys = List.map (ty defenv impl env) al in
ty_app ts tys ty_app ts tys
| Edef (dw,args) -> | Edef (dw,al) ->
let ts = match dw with let ts = match dw with
| DT DTuniv -> ts_univ | DT DTuniv -> ts_univ
| DT DTint | DT DTint
...@@ -138,12 +140,73 @@ let rec ty defenv impl env { e_loc = loc; e_node = n } = match n with ...@@ -138,12 +140,73 @@ let rec ty defenv impl env { e_loc = loc; e_node = n } = match n with
| DT DTreal -> assert false (* TODO: arithmetic *) | DT DTreal -> assert false (* TODO: arithmetic *)
| DT DTdummy -> error ~loc InvalidDummy | DT DTdummy -> error ~loc InvalidDummy
| DT DTtype | DT DTprop | DF _ | DP _ -> error ~loc TypeExpected in | DT DTtype | DT DTprop | DF _ | DP _ -> error ~loc TypeExpected in
let tys = List.map (ty defenv impl env) args in let tys = List.map (ty defenv impl env) al in
ty_app ts tys ty_app ts tys
| Evar v -> | Evar v ->
ty_var (find_tv ~loc impl env v) ty_var (find_tv ~loc impl env v)
| Elet _ | Eite _ | Eqnt _ | Ebin _ | Elet _ | Eite _ | Eqnt _ | Ebin _
| Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected | Enot _ | Eequ _ | Edob _ | Enum _ -> error ~loc TypeExpected
(*
let rec term defenv impl env { e_loc = loc; e_node = n } = match n with
| Eapp (aw,al) ->
begin match find_fs ~loc impl env aw al with
| SFunc (tvl,fs) ->
let rec args tvm tvl al = match tvl,al with
| (tv::tvl),(a::al) ->
let ty = ty defenv impl env a in
let tvm = Mtv.add tv ty tvm in
args tvm tvl al
| [],al ->
(* TODO: type checking + dummies *)
let ty = option_map (ty_inst tvm) fs.ls_value in
let tl = List.map (term defenv impl env) al in
t_app fs tl ty
| _ -> error ~loc BadArity
in
args Mtv.empty tvl al
| SletF (tvl,vl,e) ->
let rec args tvm vm tvl vl al = match tvl,vl,al with
| (tv::tvl),_,(a::al) ->
let ty = ty defenv impl env a in
let tvm = Mtv.add tv ty tvm in
args tvm vm tvl vl al
| _,(v::vl),(a::al) ->
let t = term defenv impl env a in
let vm = Mvs.add v t vm in
args tvm vm tvl vl al
| [],[],[] ->
t_ty_subst tvm vm e
| _ -> error ~loc BadArity
in
args Mtv.empty Mvs.empty tvl vl al
| SVar v ->
t_var v
| _ -> error ~loc TermExpected
end
| Edef (dw,al) ->
let fs = match dw with
| DF _ -> assert false (* TODO: arithmetic *)
| DT DTdummy -> error ~loc InvalidDummy
| DT _ | DP _ -> error ~loc TermExpected in
let tl = List.map (term defenv impl env) al in
t_app_infer fs tl
| Evar v ->
t_var (find_vs ~loc impl env v)
| Edob _ ->
(* TODO: distinct objects *)
assert false
| Enum _ ->
(* TODO: arithmetic *)
assert false
| Elet (def,e) ->
| Eite (cn,th,el) ->
let cn = fmla defenv impl env cn in
let th = term defenv impl env th in
let el = term defenv impl env el in
t_if cn th el
| Eqnt _ | Ebin _ | Enot _ | Eequ _ -> error ~loc TermExpected
*)
let typecheck _env _path _ast = Mstr.empty let typecheck _env _path _ast = Mstr.empty
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment