From ae326f646ef4c01b43d6da04201b427d1e175400 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 3 Dec 2001 15:13:22 +0000 Subject: [PATCH] * Major code cleanup. * Bug fixing: discharging of objects depending on variables with a body is now handled (more) correctly. --- helm/ocaml/cic/.depend | 4 +- helm/ocaml/cic/cic.ml | 60 ++---- helm/ocaml/cic/cicParser.ml | 17 +- helm/ocaml/cic/cicParser.mli | 11 +- helm/ocaml/cic/cicParser2.ml | 30 +-- helm/ocaml/cic/cicParser3.ml | 114 +++------- helm/ocaml/cic/cicParser3.mli | 2 - helm/ocaml/cic/deannotate.ml | 42 ++-- helm/ocaml/cic_annotations/.depend | 10 +- helm/ocaml/cic_annotations/Makefile | 4 +- .../cic_annotations/cicAnnotation2Xml.ml | 194 +++++------------- .../cic_annotations/cicAnnotation2Xml.mli | 4 +- .../cic_annotations/cicAnnotationParser.ml | 4 +- .../cic_annotations/cicAnnotationParser.mli | 2 +- .../cic_annotations/cicAnnotationParser2.ml | 83 +++----- .../cic_annotations/cicAnnotationParser2.mli | 5 +- helm/ocaml/cic_annotations/cicXPath.ml | 129 ++++++++---- helm/ocaml/cic_annotations/cicXPath.mli | 4 +- helm/ocaml/cic_annotations_cache/cicCache.ml | 18 +- helm/ocaml/cic_annotations_cache/cicCache.mli | 2 +- helm/ocaml/cic_cache/cicCache.ml | 9 +- helm/ocaml/cic_proof_checking/cicCooking.ml | 10 +- .../cic_proof_checking/cicEnvironment.ml | 62 +----- .../cic_proof_checking/cicEnvironment.mli | 16 -- helm/ocaml/cic_proof_checking/cicPp.ml | 20 +- helm/ocaml/cic_proof_checking/cicReduction.ml | 39 ++-- .../cic_proof_checking/cicTypeChecker.ml | 28 +-- 27 files changed, 330 insertions(+), 593 deletions(-) diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index b5cfa7d59..591cea8df 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -8,5 +8,5 @@ cicParser3.cmo: cic.cmo cicParser3.cmi cicParser3.cmx: cic.cmx cicParser3.cmi cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi -cicParser.cmo: cicParser2.cmi cicParser3.cmi cicParser.cmi -cicParser.cmx: cicParser2.cmx cicParser3.cmx cicParser.cmi +cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi +cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 5c42f9e76..64b7f857c 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -93,57 +93,41 @@ and coInductiveFun = string * term * term (* name, type, body *) and annterm = - ARel of id * annotation option ref * - int * string option (* DeBrujin index, binder *) - | AVar of id * annotation option ref * - UriManager.uri (* uri *) - | AMeta of id * annotation option ref * int (* numeric id *) - | ASort of id * annotation option ref * sort (* sort *) - | AImplicit of id * annotation option ref (* *) - | ACast of id * annotation option ref * - annterm * annterm (* value, type *) - | AProd of id * annotation option ref * - 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 * - UriManager.uri * int (* uri, number of cookings*) - | AAbst of id * annotation option ref * - UriManager.uri (* uri *) - | AMutInd of id * annotation option ref * - UriManager.uri * int * int (* uri, cookingsno, typeno*) - | AMutConstruct of id * annotation option ref * - UriManager.uri * int * (* uri, cookingsno, *) + ARel of id * int * string (* DeBrujin index, binder *) + | AVar of id * UriManager.uri (* uri *) + | AMeta of id * int (* numeric id *) + | ASort of id * sort (* sort *) + | AImplicit of id (* *) + | ACast of id * annterm * annterm (* value, type *) + | AProd of id * name * annterm * annterm (* binder, source, target *) + | ALambda of id * name * annterm * annterm (* binder, source, target *) + | ALetIn of id * name * annterm * annterm (* binder, term, target *) + | AAppl of id * annterm list (* arguments *) + | AConst of id * UriManager.uri * int (* uri, number of cookings*) + | AAbst of id * UriManager.uri (* uri *) + | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*) + | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *) int * int (* typeno, consno *) (*CSC: serve cookingsno?*) - | AMutCase of id * annotation option ref * - UriManager.uri * int * (* ind. uri, cookingsno *) + | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *) int * (* ind. typeno, *) annterm * annterm * (* outtype, ind. term *) annterm list (* patterns *) - | AFix of id * annotation option ref * - int * anninductiveFun list (* funno, functions *) - | ACoFix of id * annotation option ref * - int * anncoInductiveFun list (* funno, functions *) + | AFix of id * int * anninductiveFun list (* funno, functions *) + | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) and annobj = - ADefinition of id * annotation option ref * - string * (* id, *) + ADefinition of id * string * (* id, *) annterm * annterm * (* value, type, *) (int * UriManager.uri list) list exactness (* parameters *) - | AAxiom of id * annotation option ref * - string * annterm * (* id, type *) + | AAxiom of id * string * annterm * (* id, type *) (int * UriManager.uri list) list (* parameters *) - | AVariable of id * annotation option ref * + | AVariable of id * string * annterm option * annterm (* name, body, type *) - | ACurrentProof of id * annotation option ref * + | ACurrentProof of id * string * (int * annterm) list * (* name, conjectures, *) annterm * annterm (* value, type *) | AInductiveDefinition of id * - annotation option ref * anninductiveType list * (* inductive types , *) + anninductiveType list * (* inductive types , *) (int * UriManager.uri list) list * int (* parameters,n ind. pars*) and anninductiveType = string * bool * annterm * (* typename, inductive, arity *) diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index bf75243ec..f0d3e800f 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -64,18 +64,14 @@ let tokens_of_uri uri = ;; (* given the filename of an xml file of a cic object it returns its internal *) -(* representation. process_annotations is true if the annotations do really *) -(* matter *) -let term_of_xml filename uri process_annotations = +(* representation. *) +let annobj_of_xml filename uri = let module Y = Pxp_yacc in try let d = (* sets the current base uri to resolve relative URIs *) CicParser3.current_sp := tokens_of_uri uri ; CicParser3.current_uri := uri ; - CicParser3.process_annotations := process_annotations ; - CicParser3.ids_to_targets := - if process_annotations then Some (Hashtbl.create 500) else None ; let config = {Y.default_config with Y.warner = new warner} in Y.parse_document_entity config (*PXP (Y.ExtID (Pxp_types.System filename, @@ -83,13 +79,14 @@ let term_of_xml filename uri process_annotations = *) (PxpUriResolver.from_file filename) CicParser3.domspec in - let ids_to_targets = !CicParser3.ids_to_targets in - let res = (CicParser2.get_term d#root, ids_to_targets) in - CicParser3.ids_to_targets := None ; (* let's help the GC *) - res + CicParser2.get_term d#root with e -> print_endline ("Filename: " ^ filename ^ "\nException: ") ; print_endline (Pxp_types.string_of_exn e) ; raise e ;; + +let obj_of_xml filename uri = + Deannotate.deannotate_obj (annobj_of_xml filename uri) +;; diff --git a/helm/ocaml/cic/cicParser.mli b/helm/ocaml/cic/cicParser.mli index 0078f6f33..1eb5a043b 100644 --- a/helm/ocaml/cic/cicParser.mli +++ b/helm/ocaml/cic/cicParser.mli @@ -37,8 +37,9 @@ (******************************************************************************) (* given the filename of an xml file of a cic object and it's uri, it returns *) -(* its internal annotated representation. The boolean is set to true if the *) -(* annotations do really matter *) -val term_of_xml : - string -> UriManager.uri -> bool -> - Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option +(* its internal annotated representation. *) +val annobj_of_xml : string -> UriManager.uri -> Cic.annobj + +(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* its internal logical representation. *) +val obj_of_xml : string -> UriManager.uri -> Cic.obj diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 562f79bba..0dbf9f410 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -126,14 +126,6 @@ let get_content n = | _ -> raise (IllFormedXml 1) ;; -let register_id id node = - if !CicParser3.process_annotations then - match !CicParser3.ids_to_targets with - None -> assert false - | Some ids_to_targets -> - Hashtbl.add ids_to_targets id (Cic.Object node) -;; - (* Functions that, given the list of sons of a node of the cic dom (objects *) (* level), retrieve the internal representation associated to the node. *) (* Everytime a cic term subtree is found, it is translated to the internal *) @@ -231,37 +223,27 @@ let rec get_term n = (v'#extension#to_cic_term, t'#extension#to_cic_term) | _ -> raise (IllFormedXml 6) and xid = string_of_attr (n#attribute "id") in - let res = C.ADefinition (xid, ref None, id, value, typ, params) in - register_id xid res ; - res + C.ADefinition (xid, id, value, typ, params) | D.T_element "Axiom" -> let id = string_of_attr (n # attribute "name") and params = uri_list_of_attr (n # attribute "params") and typ = (get_content (get_content n))#extension#to_cic_term and xid = string_of_attr (n#attribute "id") in - let res = C.AAxiom (xid, ref None, id, typ, params) in - register_id xid res ; - res + C.AAxiom (xid, id, typ, params) | D.T_element "CurrentProof" -> let name = string_of_attr (n#attribute "name") and xid = string_of_attr (n#attribute "id") in let sons = n#sub_nodes in let (conjs, value, typ) = get_conjs_value_type sons in - let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in - register_id xid res ; - res + C.ACurrentProof (xid, name, conjs, value, typ) | D.T_element "InductiveDefinition" -> let sons = n#sub_nodes and xid = string_of_attr (n#attribute "id") in let inductiveTypes = get_inductive_types sons and params = uri_list_of_attr (n#attribute "params") and nparams = int_of_attr (n#attribute "noParams") in - let res = - C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams) - in - register_id xid res ; - res + C.AInductiveDefinition (xid, inductiveTypes, params, nparams) | D.T_element "Variable" -> let name = string_of_attr (n#attribute "name") and xid = string_of_attr (n#attribute "id") @@ -279,9 +261,7 @@ let rec get_term n = (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 + C.AVariable (xid,name,body,typ) | D.T_element _ | D.T_data | _ -> diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index ff356b13e..82ca49692 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -41,9 +41,6 @@ exception IllFormedXml of int;; -(* The hashtable from the current identifiers to the object or the terms *) -let ids_to_targets = ref None;; - (* The list of tokens of the current section path. *) (* Used to resolve relative URIs *) let current_sp = ref [];; @@ -51,9 +48,6 @@ let current_sp = ref [];; (* The uri of the object been parsed *) let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; -(* True if annotation really matter *) -let process_annotations = ref false;; - (* Utility functions to map a markup attribute to something useful *) let cic_attr_of_xml_attr = @@ -86,18 +80,10 @@ let string_of_xml_attr = let binder_of_xml_attr = function - Pxp_types.Value s -> if !process_annotations then Some s else None + Pxp_types.Value s -> s | _ -> raise (IllFormedXml 17) ;; -let register_id id node = - if !process_annotations then - match !ids_to_targets with - None -> assert false - | Some ids_to_targets -> - Hashtbl.add ids_to_targets id (Cic.Term node) -;; - (* the "interface" of the class linked to each node of the dom tree *) class virtual cic_term = @@ -176,9 +162,7 @@ class eltype_fix = | _ -> raise (IllFormedXml 13) ) sons in - let res = Cic.AFix (id, ref None, nofun, functions) in - register_id id res ; - res + Cic.AFix (id, nofun, functions) end ;; @@ -209,9 +193,7 @@ class eltype_cofix = | _ -> raise (IllFormedXml 15) ) sons in - let res = Cic.ACoFix (id, ref None, nofun, functions) in - register_id id res ; - res + Cic.ACoFix (id, nofun, functions) end ;; @@ -223,9 +205,7 @@ class eltype_implicit = method to_cic_term = let n = self#node in let id = string_of_xml_attr (n#attribute "id") in - let res = Cic.AImplicit (id, ref None) in - register_id id res ; - res + Cic.AImplicit id end ;; @@ -239,9 +219,7 @@ class eltype_rel = let value = int_of_xml_attr (n#attribute "value") and binder = binder_of_xml_attr (n#attribute "binder") and id = string_of_xml_attr (n#attribute "id") in - let res = Cic.ARel (id,ref None,value,binder) in - register_id id res ; - res + Cic.ARel (id,value,binder) end ;; @@ -254,9 +232,7 @@ class eltype_meta = let n = self#node in let value = int_of_xml_attr (n#attribute "no") and id = string_of_xml_attr (n#attribute "id") in - let res = Cic.AMeta (id,ref None,value) in - register_id id res ; - res + Cic.AMeta (id,value) end ;; @@ -280,15 +256,11 @@ class eltype_var = in aux (List.length !current_sp - n,!current_sp) in - let res = - Cic.AVar - (xid,ref None, - (UriManager.uri_of_string - ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) - ) - in - register_id id res ; - res + Cic.AVar + (xid, + (UriManager.uri_of_string + ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) + ) | _ -> raise (IllFormedXml 18) end ;; @@ -304,12 +276,8 @@ class eltype_apply = and id = string_of_xml_attr (n#attribute "id") in if List.length children < 2 then raise (IllFormedXml 8) else - let res = - Cic.AAppl - (id,ref None,List.map (fun x -> x#extension#to_cic_term) children) - in - register_id id res ; - res + Cic.AAppl + (id,List.map (fun x -> x#extension#to_cic_term) children) end ;; @@ -328,9 +296,7 @@ class eltype_cast = ty#node_type = Pxp_document.T_element "type" -> let term = te#extension#to_cic_term and typ = ty#extension#to_cic_term in - let res = Cic.ACast (id,ref None,term,typ) in - register_id id res ; - res + Cic.ACast (id,term,typ) | _ -> raise (IllFormedXml 9) end ;; @@ -344,9 +310,7 @@ class eltype_sort = let n = self#node in let sort = cic_sort_of_xml_attr (n#attribute "value") and id = string_of_xml_attr (n#attribute "id") in - let res = Cic.ASort (id,ref None,sort) in - register_id id res ; - res + Cic.ASort (id,sort) end ;; @@ -359,9 +323,7 @@ class eltype_abst = let n = self#node in let value = uri_of_xml_attr (n#attribute "uri") and id = string_of_xml_attr (n#attribute "id") in - let res = Cic.AAbst (id,ref None,value) in - register_id id res ; - res + Cic.AAbst (id,value) end ;; @@ -375,11 +337,7 @@ class eltype_const = let n = self#node in let value = uri_of_xml_attr (n#attribute "uri") and id = string_of_xml_attr (n#attribute "id") in - let res = - Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0) - in - register_id id res ; - res + Cic.AConst (id,value, U.relative_depth !current_uri value 0) end ;; @@ -394,12 +352,8 @@ class eltype_mutind = let name = uri_of_xml_attr (n#attribute "uri") and noType = int_of_xml_attr (n#attribute "noType") and id = string_of_xml_attr (n#attribute "id") in - let res = - Cic.AMutInd - (id,ref None,name, U.relative_depth !current_uri name 0, noType) - in - register_id id res ; - res + Cic.AMutInd + (id,name, U.relative_depth !current_uri name 0, noType) end ;; @@ -415,13 +369,9 @@ class eltype_mutconstruct = and noType = int_of_xml_attr (n#attribute "noType") and noConstr = int_of_xml_attr (n#attribute "noConstr") and id = string_of_xml_attr (n#attribute "id") in - let res = - Cic.AMutConstruct - (id, ref None, name, U.relative_depth !current_uri name 0, - noType, noConstr) - in - register_id id res ; - res + Cic.AMutConstruct + (id, name, U.relative_depth !current_uri name 0, + noType, noConstr) end ;; @@ -441,9 +391,7 @@ class eltype_prod = 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.AProd (id,ref None,name,source,target) in - register_id id res ; - res + Cic.AProd (id,name,source,target) | _ -> raise (IllFormedXml 10) end ;; @@ -468,12 +416,8 @@ class eltype_mutcase = and inductiveTerm = te#extension#to_cic_term and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns in - let res = - Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0, - typeno,inductiveType,inductiveTerm,lpattern) - in - register_id id res ; - res + Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0, + typeno,inductiveType,inductiveTerm,lpattern) | _ -> raise (IllFormedXml 11) end ;; @@ -494,9 +438,7 @@ class eltype_lambda = 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.ALambda (id,ref None,name,source,target) in - register_id id res ; - res + Cic.ALambda (id,name,source,target) | _ -> raise (IllFormedXml 12) end ;; @@ -517,9 +459,7 @@ class eltype_letin = 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 + Cic.ALetIn (id,name,source,target) | _ -> raise (IllFormedXml 12) end ;; diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli index ada1b2e81..990346e82 100644 --- a/helm/ocaml/cic/cicParser3.mli +++ b/helm/ocaml/cic/cicParser3.mli @@ -41,10 +41,8 @@ exception IllFormedXml of int -val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref val current_sp : string list ref val current_uri : UriManager.uri ref -val process_annotations : bool ref (* the "interface" of the class linked to each node of the dom tree *) class virtual cic_term : diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index 00d4854db..2445c3771 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -30,30 +30,30 @@ exception NotExpectingPossibleParameters;; let rec deannotate_term = let module C = Cic in function - C.ARel (_,_,n,_) -> C.Rel n - | C.AVar (_,_,uri) -> C.Var uri - | C.AMeta (_,_,n) -> C.Meta n - | C.ASort (_,_,s) -> C.Sort s + C.ARel (_,n,_) -> C.Rel n + | C.AVar (_,uri) -> C.Var uri + | C.AMeta (_,n) -> C.Meta n + | C.ASort (_,s) -> C.Sort s | C.AImplicit _ -> C.Implicit - | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) - | C.AProd (_,_,name,so,ta) -> + | C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty) + | C.AProd (_,name,so,ta) -> C.Prod (name, deannotate_term so, deannotate_term ta) - | C.ALambda (_,_,name,so,ta) -> + | C.ALambda (_,name,so,ta) -> C.Lambda (name, deannotate_term so, deannotate_term ta) - | C.ALetIn (_,_,name,so,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 - | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i) - | C.AMutConstruct (_,_,uri,cookingsno,i,j) -> + | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l) + | C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno) + | C.AAbst (_,uri) -> C.Abst uri + | C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i) + | C.AMutConstruct (_,uri,cookingsno,i,j) -> C.MutConstruct (uri,cookingsno,i,j) - | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) -> + | C.AMutCase (_,uri,cookingsno,i,outtype,te,pl) -> C.MutCase (uri,cookingsno,i,deannotate_term outtype, deannotate_term te, List.map deannotate_term pl) - | C.AFix (_,_,funno,ifl) -> + | C.AFix (_,funno,ifl) -> C.Fix (funno, List.map deannotate_inductiveFun ifl) - | C.ACoFix (_,_,funno,ifl) -> + | C.ACoFix (_,funno,ifl) -> C.CoFix (funno, List.map deannotate_coinductiveFun ifl) and deannotate_inductiveFun (name,index,ty,bo) = @@ -71,7 +71,7 @@ let deannotate_inductiveType (name, isinductive, arity, cons) = let deannotate_obj = let module C = Cic in function - C.ADefinition (_, _, id, bo, ty, params) -> + C.ADefinition (_, id, bo, ty, params) -> (match params with C.Possible params -> if !expect_possible_parameters then @@ -81,18 +81,18 @@ let deannotate_obj = | C.Actual params -> C.Definition (id, deannotate_term bo, deannotate_term ty, params) ) - | C.AAxiom (_, _, id, ty, params) -> + | C.AAxiom (_, id, ty, params) -> C.Axiom (id, deannotate_term ty, params) - | C.AVariable (_, _, name, bo, 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.ACurrentProof (_, name, conjs, bo, ty) -> C.CurrentProof ( name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs, deannotate_term bo, deannotate_term ty ) - | C.AInductiveDefinition (_, _, tys, params, parno) -> + | C.AInductiveDefinition (_, tys, params, parno) -> C.InductiveDefinition ( List.map deannotate_inductiveType tys, params, parno) ;; diff --git a/helm/ocaml/cic_annotations/.depend b/helm/ocaml/cic_annotations/.depend index 267924e89..2c30fa7d7 100644 --- a/helm/ocaml/cic_annotations/.depend +++ b/helm/ocaml/cic_annotations/.depend @@ -1,10 +1,8 @@ -cicAnnotation2Xml.cmo: cicAnnotation2Xml.cmi -cicAnnotation2Xml.cmx: cicAnnotation2Xml.cmi -cicAnnotationHinter.cmo: cicAnnotationHinter.cmi -cicAnnotationHinter.cmx: cicAnnotationHinter.cmi +cicXPath.cmo: cicXPath.cmi +cicXPath.cmx: cicXPath.cmi +cicAnnotation2Xml.cmo: cicXPath.cmi cicAnnotation2Xml.cmi +cicAnnotation2Xml.cmx: cicXPath.cmx cicAnnotation2Xml.cmi cicAnnotationParser2.cmo: cicAnnotationParser2.cmi cicAnnotationParser2.cmx: cicAnnotationParser2.cmi cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi -cicXPath.cmo: cicXPath.cmi -cicXPath.cmx: cicXPath.cmi diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile index 1627b11e3..865e6c406 100644 --- a/helm/ocaml/cic_annotations/Makefile +++ b/helm/ocaml/cic_annotations/Makefile @@ -2,8 +2,8 @@ PACKAGE = cic_annotations REQUIRES = helm-cic helm-xml PREDICATES = -INTERFACE_FILES = cicAnnotation2Xml.mli cicAnnotationParser2.mli \ - cicAnnotationParser.mli cicXPath.mli +INTERFACE_FILES = cicXPath.mli cicAnnotation2Xml.mli cicAnnotationParser2.mli \ + cicAnnotationParser.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 5a8adfaff..8d12434cb 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -29,121 +29,57 @@ exception NotImplemented;; let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";; +let get_ann ids_to_annotations = + CicXPath.get_annotation ids_to_annotations +;; + +let print_ann i2a id = + let module X = Xml in + let ann = get_ann i2a id in + match ann with + None -> [<>] + | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) +;; + (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -let print_term = +let print_term i2a = let rec aux = let module C = Cic in let module X = Xml in let module U = UriManager in function - C.ARel (id,ann,_,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.AVar (id,ann,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.AMeta (id,ann,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.ASort (id,ann,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) + C.ARel (id,_,_) -> print_ann i2a id + | C.AVar (id,_) -> print_ann i2a id + | C.AMeta (id,_) -> print_ann i2a id + | C.ASort (id,_) -> print_ann i2a id | C.AImplicit _ -> raise NotImplemented - | C.AProd (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.ACast (id,ann,v,t) -> - [< (match !ann with - None -> [<>] - | Some ann -> - (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) ; - aux v ; - aux t - >] - | C.ALambda (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.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 -> [<>] - | Some ann -> - (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) ; + | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] + | C.ACast (id,v,t) -> [< print_ann i2a id ; aux v ; aux t >] + | C.ALambda (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] + | C.ALetIn (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] + | C.AAppl (id,li) -> + [< print_ann i2a id ; List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>] >] - | C.AConst (id,ann,_,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.AAbst (id,ann,_) -> raise NotImplemented - | C.AMutInd (id,ann,_,_,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.AMutConstruct (id,ann,_,_,_,_) -> - (match !ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) - | C.AMutCase (id,ann,_,_,_,ty,te,patterns) -> - [< (match !ann with - None -> [<>] - | Some ann -> - (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) ; + | C.AConst (id,_,_) -> print_ann i2a id + | C.AAbst (id,_) -> raise NotImplemented + | C.AMutInd (id,_,_,_) -> print_ann i2a id + | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id + | C.AMutCase (id,_,_,_,ty,te,patterns) -> + [< print_ann i2a id ; aux ty ; aux te ; List.fold_right (fun x i -> [< aux x ; i>]) patterns [<>] >] - | C.AFix (id, ann, _, funs) -> - [< (match !ann with - None -> [<>] - | Some ann -> - (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) ; + | C.AFix (id,_,funs) -> + [< print_ann i2a id ; List.fold_right (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] >] - | C.ACoFix (id, ann,no,funs) -> - [< (match !ann with - None -> [<>] - | Some ann -> - (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann)) - ) ; + | C.ACoFix (id,no,funs) -> + [< print_ann i2a id ; List.fold_right (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] >] @@ -151,14 +87,14 @@ let print_term = aux ;; -let print_mutual_inductive_type (_,_,arity,constructors) = - [< print_term arity ; +let print_mutual_inductive_type i2a (_,_,arity,constructors) = + [< print_term i2a arity ; List.fold_right - (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>] + (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>] >] ;; -let pp_annotation obj curi = +let pp_annotation obj i2a curi = let module C = Cic in let module X = Xml in [< X.xml_cdata "\n" ; @@ -167,55 +103,29 @@ let pp_annotation obj curi = ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] begin match obj with - C.ADefinition (xid, ann, _, te, ty, _) -> - [< (match !ann with - None -> [<>] - | Some ann -> - X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) - ) ; - print_term te ; - print_term ty - >] - | C.AAxiom (xid, ann, _, ty, _) -> - [< (match !ann with - None -> [<>] - | Some ann -> - X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) - ) ; - print_term ty - >] - | C.AVariable (xid, ann, _, bo, ty) -> - [< (match !ann with - None -> [<>] - | Some ann -> - X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) - ) ; + C.ADefinition (xid, _, te, ty, _) -> + [< print_ann i2a xid ; print_term i2a te ; print_term i2a ty >] + | C.AAxiom (xid, _, ty, _) -> [< print_ann i2a xid ; print_term i2a ty >] + | C.AVariable (xid, _, bo, ty) -> + [< print_ann i2a xid ; (match bo with None -> [<>] - | Some bo -> print_term bo + | Some bo -> print_term i2a bo ) ; - print_term ty + print_term i2a ty >] - | C.ACurrentProof (xid, ann, _, conjs, bo, ty) -> - [< (match !ann with - None -> [<>] - | Some ann -> - X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) - ) ; + | C.ACurrentProof (xid, _, conjs, bo, ty) -> + [< print_ann i2a xid ; List.fold_right - (fun (_,t) i -> [< print_term t ; i >]) + (fun (_,t) i -> [< print_term i2a t ; i >]) conjs [<>] ; - print_term bo ; - print_term ty + print_term i2a bo ; + print_term i2a ty >] - | C.AInductiveDefinition (xid, ann, tys, params, paramsno) -> - [< (match !ann with - None -> [<>] - | Some ann -> - X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann) - ) ; + | C.AInductiveDefinition (xid, tys, params, paramsno) -> + [< print_ann i2a xid ; List.fold_right - (fun x i -> [< print_mutual_inductive_type x ; i >]) + (fun x i -> [< print_mutual_inductive_type i2a x ; i >]) tys [< >] >] end diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli b/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli index ba1b406b4..69faf6e60 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli @@ -33,4 +33,6 @@ (* *) (******************************************************************************) -val pp_annotation : Cic.annobj -> UriManager.uri -> Xml.token Stream.t +val pp_annotation : + Cic.annobj -> (Cic.id, string) Hashtbl.t -> UriManager.uri -> + Xml.token Stream.t diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.ml b/helm/ocaml/cic_annotations/cicAnnotationParser.ml index 9c4a58d53..7b4fdad6a 100644 --- a/helm/ocaml/cic_annotations/cicAnnotationParser.ml +++ b/helm/ocaml/cic_annotations/cicAnnotationParser.ml @@ -35,7 +35,7 @@ class warner = exception EmptyUri;; -let annotate filename ids_to_targets = +let get_annotations filename = let module Y = Pxp_yacc in try let d = @@ -47,7 +47,7 @@ let annotate filename ids_to_targets = Y.default_spec in - CicAnnotationParser2.annotate ids_to_targets d#root + CicAnnotationParser2.get_annotations d#root with e -> print_endline (Pxp_types.string_of_exn e) ; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.mli b/helm/ocaml/cic_annotations/cicAnnotationParser.mli index 473d05fe5..582013e3e 100644 --- a/helm/ocaml/cic_annotations/cicAnnotationParser.mli +++ b/helm/ocaml/cic_annotations/cicAnnotationParser.mli @@ -33,4 +33,4 @@ (* *) (******************************************************************************) -val annotate : string -> (string, Cic.anntarget) Hashtbl.t -> unit +val get_annotations : string -> (Cic.id, string) Hashtbl.t diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.ml b/helm/ocaml/cic_annotations/cicAnnotationParser2.ml index 58edc4ca8..15d86f5cd 100644 --- a/helm/ocaml/cic_annotations/cicAnnotationParser2.ml +++ b/helm/ocaml/cic_annotations/cicAnnotationParser2.ml @@ -60,70 +60,37 @@ let rec string_of_annotations n = | _ -> raise DontKnowWhatToDo ;; -let get_annotation n = +let get_annotation_from_node n = String.concat "" (List.map string_of_annotations (n#sub_nodes)) ;; -let annotate_object ann obj = - let module C = Cic in - let rann = - match obj with - C.ADefinition (_, rann, _, _, _, _) -> rann - | C.AAxiom (_, rann, _, _, _) -> rann - | C.AVariable (_, rann, _, _, _) -> rann - | C.ACurrentProof (_, rann, _, _, _, _) -> rann - | C.AInductiveDefinition (_, rann, _, _, _) -> rann - in - rann := Some ann -;; +exception MoreThanOneAnnotationFor of Cic.id;; -let annotate_term ann term = - let module C = Cic in - let rann = - match term with - C.ARel (_, rann, _, _) -> rann - | C.AVar (_, rann, _) -> rann - | C.AMeta (_, rann, _) -> rann - | C.ASort (_, rann, _) -> rann - | C.AImplicit (_, rann) -> rann - | 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 - | C.AMutInd (_, rann, _, _, _) -> rann - | C.AMutConstruct (_, rann, _, _, _, _) -> rann - | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann - | C.AFix (_, rann, _, _) -> rann - | C.ACoFix (_, rann, _, _) -> rann - in - rann := Some ann +let set_annotation ids_to_annotations id ann = + try + ignore (Hashtbl.find ids_to_annotations id) ; + raise (MoreThanOneAnnotationFor id) + with + Not_found -> Hashtbl.add ids_to_annotations id ann ;; -let annotate ids_to_targets n = +let get_annotations n = let module D = Pxp_document in let module C = Cic in - let annotate_elem n = - let ntype = n # node_type in - match ntype with - D.T_element "Annotation" -> - let of_uri = string_of_attr (n # attribute "of") in - begin - try - match Hashtbl.find ids_to_targets of_uri with - C.Object o -> annotate_object (get_annotation n) o - | C.Term t -> annotate_term (get_annotation n) t - with - Not_found -> assert false - end - | D.T_element _ | D.T_data -> - raise (IllFormedXml 1) - | _ -> raise DontKnowWhatToDo - in - match n # node_type with - D.T_element "Annotations" -> - List.iter annotate_elem (n # sub_nodes) - | _ -> raise (IllFormedXml 2) + let ids_to_annotations = Hashtbl.create 503 in + let annotate_elem n = + let ntype = n # node_type in + match ntype with + D.T_element "Annotation" -> + let of_uri = string_of_attr (n # attribute "of") in + set_annotation ids_to_annotations of_uri (get_annotation_from_node n) + | D.T_element _ | D.T_data -> + raise (IllFormedXml 1) + | _ -> raise DontKnowWhatToDo + in + match n # node_type with + D.T_element "Annotations" -> + List.iter annotate_elem (n # sub_nodes) ; + ids_to_annotations + | _ -> raise (IllFormedXml 2) ;; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.mli b/helm/ocaml/cic_annotations/cicAnnotationParser2.mli index 80bc0f6b1..f16bb6fe8 100644 --- a/helm/ocaml/cic_annotations/cicAnnotationParser2.mli +++ b/helm/ocaml/cic_annotations/cicAnnotationParser2.mli @@ -34,8 +34,7 @@ (******************************************************************************) exception IllFormedXml of int -val annotate : - (string, Cic.anntarget) Hashtbl.t -> +val get_annotations : < node_type : Pxp_document.node_type; sub_nodes : < attribute : string -> Pxp_types.att_value; node_type : Pxp_document.node_type; @@ -48,4 +47,4 @@ val annotate : .. > list; .. > -> - unit + (Cic.id, string) Hashtbl.t diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index 776d229af..1eaf31f4e 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -33,45 +33,98 @@ (* *) (******************************************************************************) -let get_annotation_from_term annterm = - let module C = Cic in - match annterm with - C.ARel (_,ann,_,_) -> ann - | C.AVar (_,ann,_) -> ann - | C.AMeta (_,ann,_) -> ann - | C.ASort (_,ann,_) -> ann - | C.AImplicit (_,ann) -> ann - | 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 - | C.AMutInd (_,ann,_,_,_) -> ann - | C.AMutConstruct (_,ann,_,_,_,_)-> ann - | C.AMutCase (_,ann,_,_,_,_,_,_) -> ann - | C.AFix (_,ann,_,_) -> ann - | C.ACoFix (_,ann,_,_) -> ann -;; - -let get_annotation_from_obj annobj = - let module C = Cic in - match annobj with - C.ADefinition (_,ann,_,_,_,_) -> ann - | C.AAxiom (_,ann,_,_,_) -> ann - | C.AVariable (_,ann,_,_,_) -> ann - | C.ACurrentProof (_,ann,_,_,_,_) -> ann - | C.AInductiveDefinition (_,ann,_,_,_) -> ann +let get_annotation ids_to_annotations xpath = + try + Some (Hashtbl.find ids_to_annotations xpath) + with + Not_found -> None ;; -exception IdUnknown of string;; +exception MoreThanOneTargetFor of Cic.id;; -let get_annotation (annobj,ids_to_targets) xpath = - try - match Hashtbl.find ids_to_targets xpath with - Cic.Object annobj -> get_annotation_from_obj annobj - | Cic.Term annterm -> get_annotation_from_term annterm - with - Not_found -> raise (IdUnknown xpath) +let get_ids_to_targets annobj = + let module C = Cic in + let ids_to_targets = Hashtbl.create 503 in + let set_target id target = + try + ignore (Hashtbl.find ids_to_targets id) ; + raise (MoreThanOneTargetFor id) + with + Not_found -> Hashtbl.add ids_to_targets id target + in + let rec add_target_term t = + match t with + C.ARel (id,_,_) + | C.AVar (id,_) + | C.AMeta (id,_) + | C.ASort (id,_) + | C.AImplicit id -> + set_target id (C.Term t) + | C.ACast (id,va,ty) -> + set_target id (C.Term t) ; + add_target_term va ; + add_target_term ty + | C.AProd (id,_,so,ta) + | C.ALambda (id,_,so,ta) + | C.ALetIn (id,_,so,ta) -> + set_target id (C.Term t) ; + add_target_term so ; + add_target_term ta + | C.AAppl (id,l) -> + set_target id (C.Term t) ; + List.iter add_target_term l + | C.AConst (id,_,_) + | C.AAbst (id,_) + | C.AMutInd (id,_,_,_) + | C.AMutConstruct (id,_,_,_,_) -> + set_target id (C.Term t) + | C.AMutCase (id,_,_,_,ot,it,pl) -> + set_target id (C.Term t) ; + List.iter add_target_term (ot::it::pl) + | C.AFix (id,_,ifl) -> + set_target id (C.Term t) ; + List.iter + (function (_,_,ty,bo) -> + add_target_term ty ; + add_target_term bo + ) ifl + | C.ACoFix (id,_,cfl) -> + set_target id (C.Term t) ; + List.iter + (function (_,ty,bo) -> + add_target_term ty ; + add_target_term bo + ) cfl + in + let add_target_obj annobj = + match annobj with + C.ADefinition (id,_,bo,ty,_) -> + set_target id (C.Object annobj) ; + add_target_term bo ; + add_target_term ty + | C.AAxiom (id,_,ty,_) -> + set_target id (C.Object annobj) ; + add_target_term ty + | C.AVariable (id,_,None,ty) -> + set_target id (C.Object annobj) ; + add_target_term ty + | C.AVariable (id,_,Some bo,ty) -> + set_target id (C.Object annobj) ; + add_target_term bo ; + add_target_term ty + | C.ACurrentProof (id,_,cl,bo,ty) -> + set_target id (C.Object annobj) ; + List.iter (function (_,t) -> add_target_term t) cl ; + add_target_term bo ; + add_target_term ty + | C.AInductiveDefinition (id,itl,_,_) -> + set_target id (C.Object annobj) ; + List.iter + (function (_,_,arity,cl) -> + add_target_term arity ; + List.iter (function (_,ty,_) -> add_target_term ty) cl + ) itl + in + add_target_obj annobj ; + ids_to_targets ;; diff --git a/helm/ocaml/cic_annotations/cicXPath.mli b/helm/ocaml/cic_annotations/cicXPath.mli index 5ca9a2cf6..23380e02a 100644 --- a/helm/ocaml/cic_annotations/cicXPath.mli +++ b/helm/ocaml/cic_annotations/cicXPath.mli @@ -34,4 +34,6 @@ (******************************************************************************) val get_annotation : - 'a * (string, Cic.anntarget) Hashtbl.t -> string -> string option ref + (Cic.id, string) Hashtbl.t -> Cic.id -> string option + +val get_ids_to_targets : Cic.annobj -> (Cic.id, Cic.anntarget) Hashtbl.t diff --git a/helm/ocaml/cic_annotations_cache/cicCache.ml b/helm/ocaml/cic_annotations_cache/cicCache.ml index b26bddbf8..8bc4be6c4 100644 --- a/helm/ocaml/cic_annotations_cache/cicCache.ml +++ b/helm/ocaml/cic_annotations_cache/cicCache.ml @@ -39,13 +39,13 @@ let get_annobj uri = let module G = Getter in let module U = UriManager in let cicfilename = G.getxml (U.cicuri_of_uri uri) in - match CicParser.term_of_xml cicfilename uri true with - (_, None) -> assert false - | (annobj, Some ids_to_targets) -> - if U.uri_is_annuri uri then - begin - let annfilename = G.getxml (U.annuri_of_uri uri) in - CicAnnotationParser.annotate annfilename ids_to_targets - end ; - (annobj, ids_to_targets) + let annobj = CicParser.annobj_of_xml cicfilename uri in + annobj, + if U.uri_is_annuri uri then + begin + let annfilename = G.getxml (U.annuri_of_uri uri) in + Some (CicAnnotationParser.get_annotations annfilename) + end + else + None ;; diff --git a/helm/ocaml/cic_annotations_cache/cicCache.mli b/helm/ocaml/cic_annotations_cache/cicCache.mli index b4c50c6c4..160a162ec 100644 --- a/helm/ocaml/cic_annotations_cache/cicCache.mli +++ b/helm/ocaml/cic_annotations_cache/cicCache.mli @@ -34,4 +34,4 @@ (******************************************************************************) val get_annobj : - UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t + UriManager.uri -> Cic.annobj * (Cic.id, string) Hashtbl.t option diff --git a/helm/ocaml/cic_cache/cicCache.ml b/helm/ocaml/cic_cache/cicCache.ml index 7dfd8242d..adfeb0575 100644 --- a/helm/ocaml/cic_cache/cicCache.ml +++ b/helm/ocaml/cic_cache/cicCache.ml @@ -39,11 +39,12 @@ let get_annobj uri = let module G = Getter in let module U = UriManager in let cicfilename = G.getxml (U.cicuri_of_uri uri) in - match CicParser.term_of_xml cicfilename uri false with - (_, Some _) -> assert false - | (annobj, None) -> annobj + CicParser.annobj_of_xml cicfilename uri ;; let get_obj uri = - Deannotate.deannotate_obj (get_annobj uri) + let module G = Getter in + let module U = UriManager in + let cicfilename = G.getxml (U.cicuri_of_uri uri) in + CicParser.obj_of_xml cicfilename uri ;; diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml index 12c8cd15c..75f594a90 100644 --- a/helm/ocaml/cic_proof_checking/cicCooking.ml +++ b/helm/ocaml/cic_proof_checking/cicCooking.ml @@ -136,8 +136,14 @@ let cook_gen add_binder curi cookingsno ty vars = C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype) | _ -> raise (WrongUriToVariable (U.string_of_uri var)) in - cookrec (add_binder (C.Name varname) varbody vartype - (cook curi cookingsno var ty)) tl + let cooked_once = + add_binder (C.Name varname) varbody vartype + (match varbody with + Some _ -> ty + | None -> cook curi cookingsno var ty + ) + in + cookrec cooked_once tl | _ -> ty in cookrec ty vars diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index fbe5e4b26..9e57f19bc 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -87,56 +87,16 @@ let get_obj_and_type_checking_info uri n = with Not_found -> let filename = Getter.getxml uri in - let (annobj,_) = CicParser.term_of_xml filename uri false in - let obj = Deannotate.deannotate_obj annobj in - let output = Unchecked obj in - HashTable.add hashtable (uri,0) output ; - output -;; - -(* DANGEROUS!!! *) -(* USEFUL ONLY DURING THE FIXING OF THE FILES *) -(* change_obj uri (Some newobj) *) -(* maps uri to newobj in cache. *) -(* change_obj uri None *) -(* maps uri to a freeze dummy-object. *) -let change_obj uri newobj = - let newobj = - match newobj with - Some newobj' -> Unchecked newobj' - | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit)) - in - HashTable.remove hashtable (uri,0) ; - HashTable.add hashtable (uri,0) newobj + let obj = CicParser.obj_of_xml filename uri in + let output = Unchecked obj in + HashTable.add hashtable (uri,0) output ; + output ;; let is_annotation_uri uri = Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0 ;; -(* returns both the annotated and deannotated uncooked forms (plus the *) -(* map from ids to annotation targets) *) -let get_annobj_and_type_checking_info uri = - let filename = Getter.getxml uri in - match CicParser.term_of_xml filename uri true with - (_, None) -> raise Impossible - | (annobj, Some ids_to_targets) -> - (* If uri is the uri of an annotation, let's use the annotation file *) - if is_annotation_uri uri then -(* CSC: la roba annotata non dovrebbe piu' servire - AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ; -*) assert false ; - try - (annobj, ids_to_targets, HashTable.find hashtable (uri,0)) - with - Not_found -> - let obj = Deannotate.deannotate_obj annobj in - let output = Unchecked obj in - HashTable.add hashtable (uri,0) output ; - (annobj, ids_to_targets, output) -;; - - (* get_obj uri *) (* returns the cic object whose uri is uri. If the term is not just in cache, *) (* then it is parsed via CicParser.term_of_xml from the file whose name is *) @@ -148,20 +108,6 @@ let get_obj uri = | Cooked obj -> obj ;; -(* get_annobj uri *) -(* returns the cic object whose uri is uri either in annotated and *) -(* deannotated form. The term is put into the cache if it's not there yet. *) -let get_annobj uri = - let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in - let deannobj = - match deann with - Unchecked obj -> obj - | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri)) - | Cooked obj -> obj - in - (ann, ids_to_targets, deannobj) -;; - (*CSC Commento falso *) (* get_obj uri *) (* returns the cooked cic object whose uri is uri. The term must be present *) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index c3ffd6fe4..b781a5c42 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -41,22 +41,6 @@ exception CircularDependency of string;; (* the result of Getter.get uri *) val get_obj : UriManager.uri -> Cic.obj -(* get_annobj uri *) -(* returns the cic object whose uri is uri either in annotated and in *) -(* deannotated form. It returns also the map from ids to annotation targets. *) -(* The term is put in cache if it's not there yet. *) -(* The functions raise CircularDependency if asked to retrieve a Frozen object*) -val get_annobj : - UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t * Cic.obj - -(* DANGEROUS!!! *) -(* USEFUL ONLY DURING THE FIXING OF THE FILES *) -(* change_obj uri (Some newobj) *) -(* maps uri to newobj in cache. *) -(* change_obj uri None *) -(* maps uri to a freeze dummy-object. *) -val change_obj : UriManager.uri -> Cic.obj option -> unit - type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj *) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index fafbd8848..97ae6a50f 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -37,6 +37,7 @@ (******************************************************************************) exception CicPpInternalError;; +exception NotEnoughElements;; (* Utility functions *) @@ -46,13 +47,13 @@ let string_of_name = | Cic.Anonimous -> "_" ;; -(* get_nth l n returns the nth element of the list l if it exists or raise *) -(* a CicPpInternalError if l has less than n elements or n < 1 *) +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) let rec get_nth l n = match (n,l) with (1, he::_) -> he | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise CicPpInternalError + | (_,_) -> raise NotEnoughElements ;; (* pp t l *) @@ -63,10 +64,15 @@ let rec pp t l = let module C = Cic in match t with C.Rel n -> - (match get_nth l n with - C.Name s -> s - | _ -> raise CicPpInternalError - ) + begin + try + (match get_nth l n with + C.Name s -> s + | _ -> raise CicPpInternalError + ) + with + NotEnoughElements -> string_of_int (List.length l - n) + end | C.Var uri -> UriManager.name_of_uri uri | C.Meta n -> "?" ^ (string_of_int n) | C.Sort s -> diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index a6f6ee23b..e0ad91f59 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -31,27 +31,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", 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), - C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0), - C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0), - C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0), - C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0), - C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0), - C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0), - t - ) - ) - ) - ) - ) - ) - ) - ) - ) - )) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i in if !fdebug = 0 then begin @@ -74,7 +54,15 @@ let whd = let module S = CicSubstitution in function C.Rel _ as t -> if l = [] then t else C.Appl (t::l) - | C.Var _ as t -> if l = [] then t else C.Appl (t::l) + | C.Var uri as t -> + (match CicEnvironment.get_cooked_obj uri 0 with + C.Definition _ -> raise ReferenceToDefinition + | C.Axiom _ -> raise ReferenceToAxiom + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_) -> whdaux l body + ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) | C.Implicit as t -> t @@ -93,8 +81,7 @@ let whd = (match CicEnvironment.get_cooked_obj uri cookingsno with C.Definition (_,body,_,_) -> whdaux l body | C.Axiom _ -> if l = [] then t else C.Appl (t::l) - (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *) - | C.Variable _ -> if l = [] then t else C.Appl (t::l) + | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,body,_) -> whdaux l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) @@ -272,7 +259,9 @@ let are_convertible t1 t2 = | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _) | (C.Implicit, _) | (_, C.Implicit) -> raise (Impossible 3) (* we don't trust our whd ;-) *) - | (_,_) -> false + | (_,_) -> + debug t1' [t2'] "NOT-CONVERTIBLE" ; + false end in aux t1 t2 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index f2cd6265e..28089b4cc 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -63,33 +63,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", 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), - C.Prod (C.Name "-12", C.Const (U.uri_of_string "cic:/dummy-12",0), - C.Prod (C.Name "-11", C.Const (U.uri_of_string "cic:/dummy-11",0), - C.Prod (C.Name "-10", C.Const (U.uri_of_string "cic:/dummy-10",0), - 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), - C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0), - C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0), - C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0), - C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0), - C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0), - C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0), - t - ) - ) - ) - ) - ) - ) - ) - ) - ))))))) - )) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i in if !fdebug = 0 then raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) "")) -- 2.39.2