From b276e71d04d5bc981b710b2ba793ccf157c256d7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Dec 2000 16:02:07 +0000 Subject: [PATCH] First very partial implementation of LetIn and bodyed Variables --- helm/interface/annotation2Xml.ml | 15 +++++++++- helm/interface/annotationParser2.ml | 3 +- helm/interface/cic.ml | 7 +++-- helm/interface/cic2Xml.ml | 16 ++++++++-- helm/interface/cicAnnotationHinter.ml | 27 ++++++++++++++--- helm/interface/cicCache.ml | 2 +- helm/interface/cicCooking.ml | 20 +++++++++---- helm/interface/cicParser.ml | 1 + helm/interface/cicParser2.ml | 26 +++++++++++++---- helm/interface/cicParser3.ml | 24 +++++++++++++++ helm/interface/cicPp.ml | 7 +++-- helm/interface/cicReduction.ml | 2 +- helm/interface/cicTypeChecker.ml | 42 +++++++++++++++++++++++---- helm/interface/cicXPath.ml | 3 +- helm/interface/deannotate.ml | 8 +++-- 15 files changed, 169 insertions(+), 34 deletions(-) diff --git a/helm/interface/annotation2Xml.ml b/helm/interface/annotation2Xml.ml index a9fca071a..4bcdcdaf1 100644 --- a/helm/interface/annotation2Xml.ml +++ b/helm/interface/annotation2Xml.ml @@ -61,6 +61,15 @@ let print_term = aux s ; aux t >] + | C.ALetIn (id,ann,_,s,t) -> + [< (match !ann with + None -> [<>] + | Some ann -> + (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) + ) ; + aux s ; + aux t + >] | C.AAppl (id,ann,li) -> [< (match !ann with None -> [<>] @@ -155,12 +164,16 @@ let pp_annotation obj curi = ) ; print_term ty >] - | C.AVariable (xid, ann, _, ty) -> + | C.AVariable (xid, ann, _, bo, ty) -> [< (match !ann with None -> [<>] | Some ann -> X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) ) ; + (match bo with + None -> [<>] + | Some bo -> print_term bo + ) ; print_term ty >] | C.ACurrentProof (xid, ann, _, conjs, bo, ty) -> diff --git a/helm/interface/annotationParser2.ml b/helm/interface/annotationParser2.ml index 5e5042efa..58ee1c134 100644 --- a/helm/interface/annotationParser2.ml +++ b/helm/interface/annotationParser2.ml @@ -45,7 +45,7 @@ let annotate_object ann obj = match obj with C.ADefinition (_, rann, _, _, _, _) -> rann | C.AAxiom (_, rann, _, _, _) -> rann - | C.AVariable (_, rann, _, _) -> rann + | C.AVariable (_, rann, _, _, _) -> rann | C.ACurrentProof (_, rann, _, _, _, _) -> rann | C.AInductiveDefinition (_, rann, _, _, _) -> rann in @@ -64,6 +64,7 @@ let annotate_term ann term = | C.ACast (_, rann, _, _) -> rann | C.AProd (_, rann, _, _, _) -> rann | C.ALambda (_, rann, _, _, _) -> rann + | C.ALetIn (_, rann, _, _, _) -> rann | C.AAppl (_, rann, _) -> rann | C.AConst (_, rann, _, _) -> rann | C.AAbst (_, rann, _) -> rann diff --git a/helm/interface/cic.ml b/helm/interface/cic.ml index dd9192531..1028f3287 100644 --- a/helm/interface/cic.ml +++ b/helm/interface/cic.ml @@ -33,6 +33,7 @@ and term = | Cast of term * term (* value, type *) | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) + | LetIn of name * term * term (* binder, term, target *) | Appl of term list (* arguments *) | Const of UriManager.uri * int (* uri, number of cookings*) | Abst of UriManager.uri (* uri *) @@ -51,7 +52,7 @@ and obj = (int * UriManager.uri list) list (* parameters *) | Axiom of string * term * (int * UriManager.uri list) list (* id, type, parameters *) - | Variable of string * term (* name, type *) + | Variable of string * term option * term (* name, body, type *) | CurrentProof of string * (int * term) list * (* name, conjectures, *) term * term (* value, type *) | InductiveDefinition of inductiveType list * (* inductive types, *) @@ -80,6 +81,8 @@ and annterm = name * annterm * annterm (* binder, source, target *) | ALambda of id * annotation option ref * name * annterm * annterm (* binder, source, target *) + | ALetIn of id * annotation option ref * + name * annterm * annterm (* binder, term, target *) | AAppl of id * annotation option ref * annterm list (* arguments *) | AConst of id * annotation option ref * @@ -110,7 +113,7 @@ and annobj = string * annterm * (* id, type *) (int * UriManager.uri list) list (* parameters *) | AVariable of id * annotation option ref * - string * annterm (* name, type *) + string * annterm option * annterm (* name, body, type *) | ACurrentProof of id * annotation option ref * string * (int * annterm) list * (* name, conjectures, *) annterm * annterm (* value, type *) diff --git a/helm/interface/cic2Xml.ml b/helm/interface/cic2Xml.ml index ff16e2f70..9f0cdef06 100644 --- a/helm/interface/cic2Xml.ml +++ b/helm/interface/cic2Xml.ml @@ -59,6 +59,13 @@ let print_term curi = [< X.xml_nempty "source" [] (aux s) ; X.xml_nempty "target" ["binder",id] (aux t) >] + | C.ALetIn (xid,_,C.Anonimous,s,t) -> + assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*) + | C.ALetIn (xid,_,C.Name id,s,t) -> + X.xml_nempty "LETIN" ["id",xid] + [< X.xml_nempty "term" [] (aux s) ; + X.xml_nempty "letintarget" ["binder",id] (aux t) + >] | C.AAppl (id,_,li) -> X.xml_nempty "APPLY" ["id",id] [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) @@ -175,11 +182,16 @@ let pp obj curi = ["name",id ; "params",(encode (List.rev params)) ; "id",xid] [< X.xml_nempty "type" [] (print_term curi ty) >] >] - | C.AVariable (xid, _, name, ty) -> + | C.AVariable (xid, _, name, bo, ty) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Variable" ["name",name ; "id",xid] - [< X.xml_nempty "type" [] (print_term curi ty) >] + [< (match bo with + None -> [<>] + | Some bo -> X.xml_nempty "body" [] (print_term curi bo) + ) ; + X.xml_nempty "type" [] (print_term curi ty) + >] >] | C.ACurrentProof (xid, _, name, conjs, bo, ty) -> [< X.xml_cdata "\n" ; diff --git a/helm/interface/cicAnnotationHinter.ml b/helm/interface/cicAnnotationHinter.ml index 21f30a722..88d4eb49c 100644 --- a/helm/interface/cicAnnotationHinter.ml +++ b/helm/interface/cicAnnotationHinter.ml @@ -75,6 +75,7 @@ let get_id annterm = | C.ACast (id,_,_,_) -> id | C.AProd (id,_,_,_,_) -> id | C.ALambda (id,_,_,_,_) -> id + | C.ALetIn (id,_,_,_,_) -> id | C.AAppl (id,_,_) -> id | C.AConst (id,_,_,_) -> id | C.AAbst (id,_,_) -> id @@ -127,6 +128,15 @@ let create_hint_from_term annotation_window annterm = "Body", "" ; "Type", "" |] + | C.ALetIn (id,_,_,ty,bo) -> + let boid = get_id bo + and tyid = get_id ty in + link_hints annotation_window + [| "Binder", + "" ; + "Term", "" ; + "Target", "" + |] | C.AAppl (id,_,args) -> let argsid = Array.mapi @@ -248,12 +258,21 @@ let create_hint_from_obj annotation_window annobj = "Ingredients", "" ; "Type", "" |] - | C.AVariable (id,_,_,ty) -> + | C.AVariable (id,_,_,bo,ty) -> let tyid = get_id ty in link_hints annotation_window - [| "Name", "" ; - "Type", "" - |] + (match bo with + None -> + [| "Name", "" ; + "Type", "" + |] + | Some bo -> + let boid = get_id bo in + [| "Name", "" ; + "Body", "" ; + "Type", "" + |] + ) | C.ACurrentProof (id,_,_,conjs,bo,ty) -> let boid = get_id bo and tyid = get_id ty diff --git a/helm/interface/cicCache.ml b/helm/interface/cicCache.ml index 1b8488a40..4a6b1697f 100644 --- a/helm/interface/cicCache.ml +++ b/helm/interface/cicCache.ml @@ -76,7 +76,7 @@ let change_obj uri newobj = let newobj = match newobj with Some newobj' -> Unchecked newobj' - | None -> Frozen (Cic.Variable ("frozen-dummy", Cic.Implicit)) + | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit)) in HashTable.remove hashtable (uri,0) ; HashTable.add hashtable (uri,0) newobj diff --git a/helm/interface/cicCooking.ml b/helm/interface/cicCooking.ml index 4d72fb3cb..4dbac59b1 100644 --- a/helm/interface/cicCooking.ml +++ b/helm/interface/cicCooking.ml @@ -31,6 +31,7 @@ let cook curi cookingsno var = | C.Cast (te, ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t) | C.Appl (he::tl) -> (* Get rid of C.Appl (C.Appl l1) l2 *) let newtl = List.map (aux k) tl in @@ -105,21 +106,30 @@ let cook_gen add_binder curi cookingsno ty vars = let rec cookrec ty = function var::tl -> - let (varname, vartype) = + let (varname, varbody, vartype) = match CicCache.get_obj var with - C.Variable (varname, vartype) -> (varname, vartype) + C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype) | _ -> raise (WrongUriToVariable (U.string_of_uri var)) in - cookrec (add_binder (C.Name varname) vartype (cook curi cookingsno var ty)) tl + cookrec (add_binder (C.Name varname) varbody vartype + (cook curi cookingsno var ty)) tl | _ -> ty in cookrec ty vars ;; let cook_prod = - cook_gen (fun n s t -> Cic.Prod (n,s,t)) + cook_gen (fun n b s t -> + match b with + None -> Cic.Prod (n,s,t) + | Some b -> Cic.LetIn (n,b,t) + ) and cook_lambda = - cook_gen (fun n s t -> Cic.Lambda (n,s,t)) + cook_gen (fun n b s t -> + match b with + None -> Cic.Lambda (n,s,t) + | Some b -> Cic.LetIn (n,b,t) + ) ;; (*CSC: sbagliato da rifare e completare *) diff --git a/helm/interface/cicParser.ml b/helm/interface/cicParser.ml index ec8c5efb8..a034cc2e3 100644 --- a/helm/interface/cicParser.ml +++ b/helm/interface/cicParser.ml @@ -64,6 +64,7 @@ let term_of_xml filename uri process_annotations = res with e -> + print_endline ("Filename: " ^ filename ^ "\nException: ") ; print_endline (Pxp_types.string_of_exn e) ; raise e ;; diff --git a/helm/interface/cicParser2.ml b/helm/interface/cicParser2.ml index 343e22b19..d5ee18be0 100644 --- a/helm/interface/cicParser2.ml +++ b/helm/interface/cicParser2.ml @@ -239,12 +239,26 @@ let rec get_term n = res | D.T_element "Variable" -> let name = string_of_attr (n#attribute "name") - and xid = string_of_attr (n#attribute "id") in - let typ = (get_content (get_content n))#extension#to_cic_term in - let res = C.AVariable (xid,ref None,name,typ) in - register_id xid res ; - res + and xid = string_of_attr (n#attribute "id") + and (body, typ) = + let sons = n#sub_nodes in + match sons with + [b ; t] when + b#node_type = D.T_element "body" && + t#node_type = D.T_element "type" -> + let b' = get_content b + and t' = get_content t in + (Some (b'#extension#to_cic_term), t'#extension#to_cic_term) + | [t] when t#node_type = D.T_element "type" -> + let t' = get_content t in + (None, t'#extension#to_cic_term) + | _ -> raise (IllFormedXml 6) + in + let res = C.AVariable (xid,ref None,name,body,typ) in + register_id xid res ; + res | D.T_element _ - | D.T_data -> + | D.T_data + | _ -> raise (IllFormedXml 7) ;; diff --git a/helm/interface/cicParser3.ml b/helm/interface/cicParser3.ml index d0c31b0f0..6e002b143 100644 --- a/helm/interface/cicParser3.ml +++ b/helm/interface/cicParser3.ml @@ -476,6 +476,29 @@ class eltype_lambda = end ;; +class eltype_letin = + object (self) + + inherit cic_term + + method to_cic_term = + let n = self#node in + let sons = n#sub_nodes + and id = string_of_xml_attr (n#attribute "id") in + match sons with + [s ; t] when + s#node_type = Pxp_document.T_element "term" && + t#node_type = Pxp_document.T_element "letintarget" -> + let name = cic_attr_of_xml_attr (t#attribute "binder") + and source = s#extension#to_cic_term + and target = t#extension#to_cic_term in + let res = Cic.ALetIn (id,ref None,name,source,target) in + register_id id res ; + res + | _ -> raise (IllFormedXml 12) + end +;; + (* The definition of domspec, an hashtable that maps each node type to the *) (* object that must be linked to it. Used by markup. *) @@ -493,6 +516,7 @@ let domspec = "CAST", (new D.element_impl (new eltype_cast)) ; "PROD", (new D.element_impl (new eltype_prod)) ; "LAMBDA", (new D.element_impl (new eltype_lambda)) ; + "LETIN", (new D.element_impl (new eltype_letin)) ; "APPLY", (new D.element_impl (new eltype_apply)) ; "CONST", (new D.element_impl (new eltype_const)) ; "ABST", (new D.element_impl (new eltype_abst)) ; diff --git a/helm/interface/cicPp.ml b/helm/interface/cicPp.ml index 932978664..e39a0caff 100644 --- a/helm/interface/cicPp.ml +++ b/helm/interface/cicPp.ml @@ -59,6 +59,8 @@ let rec pp t l = | C.Cast (v,t) -> pp v l | C.Lambda (b,s,t) -> "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t (b::l) + | C.LetIn (b,s,t) -> + "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l) | C.Appl li -> "(" ^ (List.fold_right @@ -160,8 +162,9 @@ let ppobj obj = ) x "" ^ match i with "" -> "" | i' -> " " ^ i' ) params "" ^ "):\n" ^ pp ty [] - | C.Variable (name, ty) -> - "Variable " ^ name ^ ":\n" ^ pp ty [] + | C.Variable (name, bo, ty) -> + "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^ + (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) | C.CurrentProof (name, conjectures, value, ty) -> "Current Proof:\n" ^ List.fold_right diff --git a/helm/interface/cicReduction.ml b/helm/interface/cicReduction.ml index 6497cd378..7b2eb0944 100644 --- a/helm/interface/cicReduction.ml +++ b/helm/interface/cicReduction.ml @@ -6,7 +6,7 @@ let debug t env s = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", + CicPp.ppobj (C.Variable ("DEBUG", None, C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0), C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0), C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0), diff --git a/helm/interface/cicTypeChecker.ml b/helm/interface/cicTypeChecker.ml index 63433937b..de9f46bfe 100644 --- a/helm/interface/cicTypeChecker.ml +++ b/helm/interface/cicTypeChecker.ml @@ -14,7 +14,7 @@ let debug t env = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", + CicPp.ppobj (C.Variable ("DEBUG", None, C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0), C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0), C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0), @@ -93,12 +93,19 @@ let rec cooked_type_of_constant uri cookingsno = and type_of_variable uri = let module C = Cic in let module R = CicReduction in + let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) match CicCache.is_type_checked uri 0 with - CicCache.CheckedObj (C.Variable (_,ty)) -> ty - | CicCache.UncheckedObj (C.Variable (_,ty)) -> + CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty + | CicCache.UncheckedObj (C.Variable (_,bo,ty)) -> (* only to check that ty is well-typed *) let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri))) + ) ; CicCache.set_type_checking_info uri ; ty | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) @@ -120,6 +127,8 @@ and does_not_occur n nn te = does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest | C.Lambda (_,so,dest) -> does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest + | C.LetIn (_,so,dest) -> + does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur n nn x) l true | C.Const _ @@ -394,6 +403,7 @@ and recursive_args n nn te = | C.Prod (_,so,de) -> (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de) | C.Lambda _ -> raise Impossible (* due to type-checking *) + | C.LetIn _ -> raise NotImplemented | C.Appl _ -> [] | C.Const _ | C.Abst _ -> raise Impossible @@ -466,6 +476,10 @@ and check_is_really_smaller_arg n nn kl x safes te = check_is_really_smaller_arg n nn kl x safes so && check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + check_is_really_smaller_arg n nn kl x safes so && + check_is_really_smaller_arg (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta | C.Appl (he::_) -> (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) (*CSC: solo perche' non abbiamo trovato controesempi *) @@ -594,6 +608,10 @@ and guarded_by_destructors n nn kl x safes = guarded_by_destructors n nn kl x safes so && guarded_by_destructors (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (_,so,ta) -> + guarded_by_destructors n nn kl x safes so && + guarded_by_destructors (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in if not (List.length tl > k) then false @@ -742,6 +760,9 @@ and guarded_by_constructors n nn h = | C.Lambda (_,so,de) -> does_not_occur n nn so && guarded_by_constructors (n + 1) (nn + 1) h de + | C.LetIn (_,so,de) -> + does_not_occur n nn so && + guarded_by_constructors (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h = 1 && List.fold_right (fun x i -> i && does_not_occur n nn x) tl true @@ -971,6 +992,10 @@ and type_of t = (* only to check if the product is well-typed *) let _ = sort_of_prod (sort1,sort2) in C.Prod (n,s,type2) + | C.LetIn (n,s,t) -> + let type1 = type_of_aux env s in + let type2 = type_of_aux (type1::env) t in + type2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux env he and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in @@ -1189,10 +1214,15 @@ let typecheck uri = debug (type_of te) [] ; if not (R.are_convertible (type_of te) ty) then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) - | C.Variable (_,ty) -> + | C.Variable (_,bo,ty) -> (* only to check that ty is well-typed *) - (*CSC [] wrong *) - let _ = type_of ty in () + let _ = type_of ty in + (match bo with + None -> () + | Some bo -> + if not (R.are_convertible (type_of bo) ty) then + raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) + ) | C.InductiveDefinition _ -> cooked_mutual_inductive_defs uri uobj ) ; diff --git a/helm/interface/cicXPath.ml b/helm/interface/cicXPath.ml index 2df970737..1c6dc0d11 100644 --- a/helm/interface/cicXPath.ml +++ b/helm/interface/cicXPath.ml @@ -19,6 +19,7 @@ let get_annotation_from_term annterm = | C.ACast (_,ann,_,_) -> ann | C.AProd (_,ann,_,_,_) -> ann | C.ALambda (_,ann,_,_,_) -> ann + | C.ALetIn (_,ann,_,_,_) -> ann | C.AAppl (_,ann,_) -> ann | C.AConst (_,ann,_,_) -> ann | C.AAbst (_,ann,_) -> ann @@ -34,7 +35,7 @@ let get_annotation_from_obj annobj = match annobj with C.ADefinition (_,ann,_,_,_,_) -> ann | C.AAxiom (_,ann,_,_,_) -> ann - | C.AVariable (_,ann,_,_) -> ann + | C.AVariable (_,ann,_,_,_) -> ann | C.ACurrentProof (_,ann,_,_,_,_) -> ann | C.AInductiveDefinition (_,ann,_,_,_) -> ann ;; diff --git a/helm/interface/deannotate.ml b/helm/interface/deannotate.ml index 658554fff..313400302 100644 --- a/helm/interface/deannotate.ml +++ b/helm/interface/deannotate.ml @@ -15,6 +15,8 @@ let rec deannotate_term = C.Prod (name, deannotate_term so, deannotate_term ta) | C.ALambda (_,_,name,so,ta) -> C.Lambda (name, deannotate_term so, deannotate_term ta) + | C.ALetIn (_,_,name,so,ta) -> + C.LetIn (name, deannotate_term so, deannotate_term ta) | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l) | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno) | C.AAbst (_,_,uri) -> C.Abst uri @@ -56,8 +58,10 @@ let deannotate_obj = ) | C.AAxiom (_, _, id, ty, params) -> C.Axiom (id, deannotate_term ty, params) - | C.AVariable (_, _, name, ty) -> - C.Variable (name, deannotate_term ty) + | C.AVariable (_, _, name, bo, ty) -> + C.Variable (name, + (match bo with None -> None | Some bo -> Some (deannotate_term bo)), + deannotate_term ty) | C.ACurrentProof (_, _, name, conjs, bo, ty) -> C.CurrentProof ( name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, -- 2.39.2