From: Claudio Sacerdoti Coen Date: Fri, 25 Oct 2002 15:14:18 +0000 (+0000) Subject: - Porting of all the code to the new DTD format (with, among others, explicit X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=08a2b1a3f1a1e9af07850089f0e0838eb052223d;p=helm.git - Porting of all the code to the new DTD format (with, among others, explicit named substitutions) - Porting to the new version of Pxp - Porting of the cicReductionMachine code (that was abandoned for a while) - Removal of all the cooking machinery - Removal of the optimization (memoization) of the computation of recursive arguments of constructors. Required to implement the next point. The actual performance loss is minimal. - First prototype of an environment with trusting abilities. Notes: unification is still untested and probably wrong w.r.t. explicit name substitutions. --- diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 2429dcfed..b2f6dd8f1 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -37,8 +37,11 @@ (* STUFF TO MANAGE IDENTIFIERS *) type id = string (* the abstract type of the (annotated) node identifiers *) +type 'term explicit_named_substitution = (UriManager.uri * 'term) list + type anntarget = - Object of annobj + Object of annobj (* if annobj is a Constant, this is its type *) + | ConstantBody of annobj | Term of annterm | Conjecture of annconjecture | Hypothesis of annhypothesis @@ -50,10 +53,11 @@ and sort = | Type and name = Name of string - | Anonimous + | Anonymous and term = Rel of int (* DeBrujin index *) - | Var of UriManager.uri (* uri *) + | Var of UriManager.uri * (* uri, *) + term explicit_named_substitution (* explicit named subst. *) | Meta of int * (term option) list (* numeric id, *) (* local context *) | Sort of sort (* sort *) @@ -63,34 +67,36 @@ and term = | 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*) - | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) - (* typeno is 0 based *) - | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) - (* consno is 1 based *) - (*CSC: serve cookingsno?*) - | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *) + | Const of UriManager.uri * (* uri, *) + term explicit_named_substitution (* explicit named subst. *) + | MutInd of UriManager.uri * int * (* uri, typeno, *) + term explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + | MutConstruct of UriManager.uri * (* uri, *) + int * int * (* typeno, consno *) + term explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + (* consno is 1 based *) + | MutCase of UriManager.uri * (* ind. uri, *) int * (* ind. typeno, *) term * term * (* outtype, ind. term *) term list (* patterns *) | Fix of int * inductiveFun list (* funno, functions *) | CoFix of int * coInductiveFun list (* funno, functions *) and obj = - Definition of string * term * term * (* id, value, type, *) - (int * UriManager.uri list) list (* parameters *) - | Axiom of string * term * - (int * UriManager.uri list) list (* id, type, parameters *) - | Variable of string * term option * term (* name, body, type *) + Constant of string * term option * term * (* id, body, type, *) + UriManager.uri list (* parameters *) + | Variable of string * term option * term * (* name, body, type *) + UriManager.uri list (* parameters *) | CurrentProof of string * metasenv * (* name, conjectures, *) - term * term (* value, type *) + term * term * UriManager.uri list (* value, type, parameters *) | InductiveDefinition of inductiveType list * (* inductive types, *) - (int * UriManager.uri list) list * int (* parameters, n ind. pars *) + UriManager.uri list * int (* parameters, n ind. pars *) and inductiveType = string * bool * term * (* typename, inductive, arity *) constructor list (* constructors *) and constructor = - string * term * bool list option ref (* id, type, really recursive *) + string * term (* id, type *) and inductiveFun = string * int * term * term (* name, ind. index, type, body *) and coInductiveFun = @@ -105,8 +111,10 @@ and annconjecture = id * int * anncontext * annterm and annmetasenv = annconjecture list and annterm = - ARel of id * int * string (* DeBrujin index, binder *) - | AVar of id * UriManager.uri (* uri *) + ARel of id * id * int * (* idref, DeBrujin index, *) + string (* binder *) + | AVar of id * UriManager.uri * (* uri, *) + annterm explicit_named_substitution (* explicit named subst. *) | AMeta of id * int * (annterm option) list (* numeric id, *) (* local context *) | ASort of id * sort (* sort *) @@ -116,47 +124,46 @@ and annterm = | 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*) - | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*) + | AConst of id * UriManager.uri * (* uri, *) + annterm explicit_named_substitution (* explicit named subst. *) + | AMutInd of id * UriManager.uri * int * (* uri, typeno *) + annterm explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + | AMutConstruct of id * UriManager.uri * (* uri, *) + int * int * (* typeno, consno *) + annterm explicit_named_substitution (* explicit named subst. *) (* typeno is 0 based *) - | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) (* consno is 1 based *) - (*CSC: serve cookingsno?*) - | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *) + | AMutCase of id * UriManager.uri * (* ind. uri, *) int * (* ind. typeno, *) annterm * annterm * (* outtype, ind. term *) annterm list (* patterns *) | AFix of id * int * anninductiveFun list (* funno, functions *) | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) and annobj = - ADefinition of id * string * (* id, *) - annterm * annterm * (* value, type, *) - (int * UriManager.uri list) list exactness (* parameters *) - | AAxiom of id * string * annterm * (* id, type *) - (int * UriManager.uri list) list (* parameters *) + AConstant of id * id option * string * (* name, *) + annterm option * annterm * (* body, type, *) + UriManager.uri list (* parameters *) | AVariable of id * - string * annterm option * annterm (* name, body, type *) - | ACurrentProof of id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm (* value, type *) + string * annterm option * annterm * (* name, body, type *) + UriManager.uri list (* parameters *) + | ACurrentProof of id * id * + string * annmetasenv * (* name, conjectures, *) + annterm * annterm * UriManager.uri list (* value,type,parameters *) | AInductiveDefinition of id * anninductiveType list * (* inductive types , *) - (int * UriManager.uri list) list * int (* parameters,n ind. pars*) + UriManager.uri list * int (* parameters,n ind. pars*) and anninductiveType = string * bool * annterm * (* typename, inductive, arity *) annconstructor list (* constructors *) and annconstructor = - string * annterm * bool list option ref (* id, type, really recursive *) + string * annterm (* id, type *) and anninductiveFun = - string * int * annterm * annterm (* name, ind. index, type, body *) + id * string * int * annterm * annterm (* name, ind. index, type, body *) and anncoInductiveFun = - string * annterm * annterm (* name, type, body *) + id * string * annterm * annterm (* name, type, body *) and annotation = string -and 'a exactness = - Possible of 'a (* an approximation to something *) - | Actual of 'a (* something *) and context_entry = (* A declaration or definition *) Decl of term diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 241a5c175..5149cfd6a 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -41,7 +41,7 @@ exception Warnings;; class warner = object method warn w = - print_endline ("WARNING: " ^ w) ; + prerr_endline ("WARNING: " ^ w) ; (raise Warnings : unit) end ;; @@ -66,28 +66,42 @@ let tokens_of_uri uri = (* given the filename of an xml file of a cic object it returns its internal *) (* representation. *) -let annobj_of_xml filename uri = +let annobj_of_xml filename filenamebody uri = let module Y = Pxp_yacc in try - let d = + let root, rootbody = (* sets the current base uri to resolve relative URIs *) CicParser3.current_sp := tokens_of_uri uri ; CicParser3.current_uri := uri ; let config = {Y.default_config with Y.warner = new warner} in - Y.parse_document_entity config -(*PXP (Y.ExtID (Pxp_types.System filename, - new Pxp_reader.resolve_as_file ~url_of_id ())) -*) (PxpUriResolver.from_file filename) - CicParser3.domspec + let doc = + Y.parse_document_entity config + (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) + CicParser3.domspec in +(* CSC: Until PXP bug is resolved *) +PxpUrlResolver.url_resolver#close_all ; + let docroot = doc#root in + match filenamebody with + None -> docroot,None + | Some filename -> + let docbody = + Y.parse_document_entity config + (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) + CicParser3.domspec + in +(* CSC: Until PXP bug is resolved *) +PxpUrlResolver.url_resolver#close_all ; + docroot,Some docbody#root in - CicParser2.get_term d#root + CicParser2.get_term root rootbody with e -> - print_endline ("Filename: " ^ filename ^ "\nException: ") ; - print_endline (Pxp_types.string_of_exn e) ; + prerr_endline ("Filenames: " ^ filename ^ + (match filenamebody with None -> "" | Some s -> ", " ^ s)) ; + prerr_endline ("Exception: " ^ Pxp_types.string_of_exn e) ; raise e ;; -let obj_of_xml filename uri = - Deannotate.deannotate_obj (annobj_of_xml filename uri) +let obj_of_xml filename filenamebody uri = + Deannotate.deannotate_obj (annobj_of_xml filename filenamebody uri) ;; diff --git a/helm/ocaml/cic/cicParser.mli b/helm/ocaml/cic/cicParser.mli index 1eb5a043b..0d0a8172b 100644 --- a/helm/ocaml/cic/cicParser.mli +++ b/helm/ocaml/cic/cicParser.mli @@ -37,9 +37,13 @@ (******************************************************************************) (* given the filename of an xml file of a cic object and it's uri, it returns *) -(* its internal annotated representation. *) -val annobj_of_xml : string -> UriManager.uri -> Cic.annobj +(* its internal annotated representation. In the case of constants (whose *) +(* type is splitted from the body), a second xml file (for the body) must be *) +(* provided. *) +val annobj_of_xml : string -> string option -> 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 +(* its internal logical representation. In the case of constants (whose *) +(* type is splitted from the body), a second xml file (for the body) must be *) +(* provided. *) +val obj_of_xml : string -> string option -> UriManager.uri -> Cic.obj diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 154b294ce..e74cf73d3 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -42,64 +42,11 @@ exception NotImplemented;; (* Utility functions that transform a Pxp attribute into something useful *) -(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *) -(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *) -let mk_absolute_uris s = - let l = (Str.split (Str.regexp ":") s) in - let absolute_of_relative n v = - let module P3 = CicParser3 in - let rec mkburi = - function - (0,_) -> "/" - | (n,he::tl) when n > 0 -> - "/" ^ he ^ mkburi (n - 1, tl) - | _ -> raise (IllFormedXml 12) - in - let m = List.length !P3.current_sp - (int_of_string n) in - let buri = mkburi (m, !P3.current_sp) in - UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var") - in - let rec absolutize = - function - [] -> [] - | [no ; vs] -> - let vars = (Str.split (Str.regexp " ") vs) in - [(int_of_string no, List.map (absolute_of_relative no) vars)] - | no::vs::tl -> - let vars = (Str.split (Str.regexp " ") vs) in - let rec add_prefix = - function - [no2] -> ([], no2) - | he::tl -> - let (pvars, no2) = add_prefix tl in - ((absolute_of_relative no he)::pvars, no2) - | _ -> raise (IllFormedXml 11) - in - let (pvars, no2) = add_prefix vars in - (int_of_string no, pvars)::(absolutize (no2::tl)) - | _ -> raise (IllFormedXml 10) - in - (* last parameter must be applied first *) - absolutize l -;; - -let option_uri_list_of_attr a1 a2 = - let module T = Pxp_types in - let parameters = - match a1 with - T.Value s -> mk_absolute_uris s - | _ -> raise (IllFormedXml 0) - in - match a2 with - T.Value "POSSIBLE" -> Cic.Possible parameters - | T.Implied_value -> Cic.Actual parameters - | _ -> raise (IllFormedXml 0) -;; - let uri_list_of_attr a = let module T = Pxp_types in match a with - T.Value s -> mk_absolute_uris s + T.Value s -> + List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s) | _ -> raise (IllFormedXml 0) ;; @@ -123,7 +70,7 @@ let name_of_attr a = let module C = Cic in match a with T.Value s -> C.Name s - | T.Implied_value -> C.Anonimous + | T.Implied_value -> C.Anonymous | _ -> raise (IllFormedXml 0) ;; @@ -145,55 +92,46 @@ let get_content n = (* dtd *) (* called when a CurrentProof is found *) -let get_conjs_value_type l = - let rec rget (c, v, t) l = +let get_conjs_value l = + let rec rget (c, v) l = let module D = Pxp_document in match l with - [] -> (c, v, t) + [] -> (c, v) | conj::tl when conj#node_type = D.T_element "Conjecture" -> let no = int_of_attr (conj#attribute "no") in - let xid = string_of_attr (conj#attribute "id") in + let id = string_of_attr (conj#attribute "id") in let typ,canonical_context = match List.rev (conj#sub_nodes) with [] -> raise (IllFormedXml 13) | typ::canonical_context -> - (get_content typ)#extension#to_cic_term, + (get_content typ)#extension#to_cic_term [], List.map (function n -> - match n#node_type with - D.T_element "Decl" -> - let name = name_of_attr (n#attribute "name") in - let hid = string_of_attr (n#attribute "id") in - let term = (get_content n)#extension#to_cic_term in - hid,Some (name,Cic.ADecl term) - | D.T_element "Def" -> - let name = name_of_attr (n#attribute "name") in - let hid = string_of_attr (n#attribute "id") in - let term = (get_content n)#extension#to_cic_term in - hid,Some (name,Cic.ADef term) - | D.T_element "Hidden" -> - let hid = string_of_attr (n#attribute "id") in - hid,None - | _ -> raise (IllFormedXml 14) + let id = string_of_attr (n#attribute "id") in + match n#node_type with + D.T_element "Decl" -> + let name = name_of_attr (n#attribute "name") in + let term = (get_content n)#extension#to_cic_term [] in + id, Some (name,Cic.ADecl term) + | D.T_element "Def" -> + let name = name_of_attr (n#attribute "name") in + let term = (get_content n)#extension#to_cic_term [] in + id, Some (name,Cic.ADef term) + | D.T_element "Hidden" -> id, None + | _ -> raise (IllFormedXml 14) ) canonical_context in - rget ((xid, no, canonical_context, typ)::c, v, t) tl + rget ((id, no, canonical_context, typ)::c, v) tl | value::tl when value#node_type = D.T_element "body" -> - let v' = (get_content value)#extension#to_cic_term in + let v' = (get_content value)#extension#to_cic_term [] in (match v with - None -> rget (c, Some v', t) tl + None -> rget (c, Some v') tl | _ -> raise (IllFormedXml 2) ) - | typ::tl when typ#node_type = D.T_element "type" -> - let t' = (get_content typ)#extension#to_cic_term in - (match t with - None -> rget (c, v, Some t') tl - | _ -> raise (IllFormedXml 3) - ) | _ -> raise (IllFormedXml 4) in - match rget ([], None, None) l with - (revc, Some v, Some t) -> (List.rev revc, v, t) + match rget ([], None) l with + (revc, Some v) -> (List.rev revc, v) | _ -> raise (IllFormedXml 5) ;; @@ -205,12 +143,12 @@ let get_names_arity_constructors l = match l with [] -> (a, c) | arity::tl when arity#node_type = D.T_element "arity" -> - let a' = (get_content arity)#extension#to_cic_term in + let a' = (get_content arity)#extension#to_cic_term [] in rget (Some a',c) tl | con::tl when con#node_type = D.T_element "Constructor" -> let id = string_of_attr (con#attribute "name") - and ty = (get_content con)#extension#to_cic_term in - rget (a,(id,ty,ref None)::c) tl + and ty = (get_content con)#extension#to_cic_term [] in + rget (a,(id,ty)::c) tl | _ -> raise (IllFormedXml 9) in match rget (None,[]) l with @@ -236,40 +174,50 @@ let rec get_inductive_types = (* representation of the cic object described in the tree *) (* It uses the previous functions and the to_cic_term method defined *) (* in cicParser3 (used for subtrees that encode cic terms) *) -let rec get_term n = +let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody += + let module U = UriManager in let module D = Pxp_document in let module C = Cic in - let ntype = n # node_type in + let ntype = n#node_type in match ntype with - D.T_element "Definition" -> - let id = string_of_attr (n # attribute "name") - and params = - option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode") - and (value, typ) = - let sons = n#sub_nodes in - match sons with - [v ; t] when - v#node_type = D.T_element "body" && - t#node_type = D.T_element "type" -> - let v' = get_content v - and t' = get_content t in - (v'#extension#to_cic_term, t'#extension#to_cic_term) - | _ -> raise (IllFormedXml 6) - and xid = string_of_attr (n#attribute "id") in - 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 - 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 - C.ACurrentProof (xid, name, conjs, value, typ) + D.T_element "ConstantType" -> + let name = string_of_attr (n # attribute "name") in + let params = uri_list_of_attr (n#attribute "params") in + let xid = string_of_attr (n#attribute "id") in + let typ = (get_content n)#extension#to_cic_term [] in + (match nbody with + None -> + (* Axiom *) + C.AConstant (xid, None, name, None, typ, params) + | Some nbody' -> + let nbodytype = nbody'#node_type in + match nbodytype with + D.T_element "ConstantBody" -> + let for_ = string_of_attr (nbody'#attribute "for") in + let paramsbody = uri_list_of_attr (nbody'#attribute "params") in + let xidbody = string_of_attr (nbody'#attribute "id") in + let value = (get_content nbody')#extension#to_cic_term [] in + if paramsbody = params && + U.eq (U.uri_of_string for_) !CicParser3.current_uri + then + C.AConstant (xid, Some xidbody, name, Some value, typ, params) + else + raise (IllFormedXml 6) + | D.T_element "CurrentProof" -> + let for_ = string_of_attr (nbody'#attribute "of") in + let xidbody = string_of_attr (nbody'#attribute "id") in + let value = (get_content nbody')#extension#to_cic_term [] in + let sons = nbody'#sub_nodes in + let (conjs, value) = get_conjs_value sons in + if U.eq (U.uri_of_string for_) !CicParser3.current_uri then + C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params) + else + raise (IllFormedXml 6) + | D.T_element _ + | D.T_data + | _ -> raise (IllFormedXml 6) + ) | D.T_element "InductiveDefinition" -> let sons = n#sub_nodes and xid = string_of_attr (n#attribute "id") in @@ -279,6 +227,7 @@ let rec get_term n = C.AInductiveDefinition (xid, inductiveTypes, params, nparams) | D.T_element "Variable" -> let name = string_of_attr (n#attribute "name") + and params = uri_list_of_attr (n#attribute "params") and xid = string_of_attr (n#attribute "id") and (body, typ) = let sons = n#sub_nodes in @@ -288,15 +237,14 @@ let rec get_term n = 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) + (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) + (None, t'#extension#to_cic_term []) | _ -> raise (IllFormedXml 6) in - C.AVariable (xid,name,body,typ) + C.AVariable (xid,name,body,typ,params) | D.T_element _ | D.T_data - | _ -> - raise (IllFormedXml 7) + | _ -> raise (IllFormedXml 7) ;; diff --git a/helm/ocaml/cic/cicParser2.mli b/helm/ocaml/cic/cicParser2.mli index be0a00054..1d95f35ee 100644 --- a/helm/ocaml/cic/cicParser2.mli +++ b/helm/ocaml/cic/cicParser2.mli @@ -41,17 +41,12 @@ exception IllFormedXml of int exception NotImplemented (* This is the main function and also the only one used directly from *) -(* cicParser. Given the root of the dom tree, it returns the internal *) -(* representation of the cic object described in the tree *) +(* cicParser. Given the root of the dom tree and, possibly, also the *) +(* root of the dom tree of the constant body, it returns the internal *) +(* representation of the cic object described in the tree(s). *) (* It uses the previous functions and the to_cic_term method defined *) (* in cicParser3 (used for subtrees that encode cic terms) *) val get_term : - < attribute : string -> Pxp_types.att_value; - node_type : Pxp_document.node_type; - sub_nodes : < attribute : string -> Pxp_types.att_value; - node_type : Pxp_document.node_type; - sub_nodes : CicParser3.cic_term Pxp_document.node list; - .. > - list; - .. > -> - Cic.annobj + CicParser3.cic_term Pxp_document.node -> + CicParser3.cic_term Pxp_document.node option -> + Cic.annobj diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 8f87504ac..04bbb9029 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -53,7 +53,7 @@ let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; let cic_attr_of_xml_attr = function Pxp_types.Value s -> Cic.Name s - | Pxp_types.Implied_value -> Cic.Anonimous + | Pxp_types.Implied_value -> Cic.Anonymous | _ -> raise (IllFormedXml 1) let cic_sort_of_xml_attr = @@ -89,7 +89,7 @@ let binder_of_xml_attr = class virtual cic_term = object (self) - (* fields and methods ever required by markup *) + (* fields and methods always required by markup *) val mutable node = (None : cic_term Pxp_document.node option) method clone = {< >} @@ -103,7 +103,8 @@ class virtual cic_term = (* a method that returns the internal representation of the tree (term) *) (* rooted in this node *) - method virtual to_cic_term : Cic.annterm + method virtual to_cic_term : + (UriManager.uri * Cic.annterm) list -> Cic.annterm end ;; @@ -113,7 +114,7 @@ class eltype_not_of_cic = inherit cic_term - method to_cic_term = raise (IllFormedXml 6) + method to_cic_term _ = raise (IllFormedXml 6) end ;; @@ -124,10 +125,11 @@ class eltype_transparent = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in match n#sub_nodes with - [ t ] -> t#extension#to_cic_term + [ t ] -> t#extension#to_cic_term [] | _ -> raise (IllFormedXml 7) end ;; @@ -139,7 +141,8 @@ class eltype_fix = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let nofun = int_of_xml_attr (n#attribute "noFun") and id = string_of_xml_attr (n#attribute "id") @@ -149,16 +152,17 @@ class eltype_fix = (function f when f#node_type = Pxp_document.T_element "FixFunction" -> let name = string_of_xml_attr (f#attribute "name") + and id = string_of_xml_attr (f#attribute "id") and recindex = int_of_xml_attr (f#attribute "recIndex") and (ty, body) = match f#sub_nodes with [t ; b] when t#node_type = Pxp_document.T_element "type" && b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term, b#extension#to_cic_term) + (t#extension#to_cic_term [], b#extension#to_cic_term []) | _ -> raise (IllFormedXml 14) in - (name, recindex, ty, body) + (id, name, recindex, ty, body) | _ -> raise (IllFormedXml 13) ) sons in @@ -171,7 +175,8 @@ class eltype_cofix = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let nofun = int_of_xml_attr (n#attribute "noFun") and id = string_of_xml_attr (n#attribute "id") @@ -181,15 +186,16 @@ class eltype_cofix = (function f when f#node_type = Pxp_document.T_element "CofixFunction" -> let name = string_of_xml_attr (f#attribute "name") + and id = string_of_xml_attr (f#attribute "id") and (ty, body) = match f#sub_nodes with [t ; b] when t#node_type = Pxp_document.T_element "type" && b#node_type = Pxp_document.T_element "body" -> - (t#extension#to_cic_term, b#extension#to_cic_term) + (t#extension#to_cic_term [], b#extension#to_cic_term []) | _ -> raise (IllFormedXml 16) in - (name, ty, body) + (id, name, ty, body) | _ -> raise (IllFormedXml 15) ) sons in @@ -202,7 +208,8 @@ class eltype_implicit = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let id = string_of_xml_attr (n#attribute "id") in Cic.AImplicit id @@ -214,12 +221,14 @@ class eltype_rel = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in 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 - Cic.ARel (id,value,binder) + and id = string_of_xml_attr (n#attribute "id") + and idref = string_of_xml_attr (n#attribute "idref") in + Cic.ARel (id,idref,value,binder) end ;; @@ -228,7 +237,8 @@ class eltype_meta = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let value = int_of_xml_attr (n#attribute "no") and id = string_of_xml_attr (n#attribute "id") @@ -239,7 +249,7 @@ class eltype_meta = (function substitution -> match substitution#sub_nodes with [] -> None - | [he] -> Some he#extension#to_cic_term + | [he] -> Some (he#extension#to_cic_term []) | _ -> raise (IllFormedXml 20) ) sons in @@ -252,27 +262,13 @@ class eltype_var = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in - let name = string_of_xml_attr (n#attribute "relUri") + let uri = uri_of_xml_attr (n#attribute "uri") and xid = string_of_xml_attr (n#attribute "id") in - match Str.split (Str.regexp ",") name with - [index; id] -> - let get_prefix n = - let rec aux = - function - (0,_) -> "/" - | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl) - | _ -> raise (IllFormedXml 19) - in - aux (List.length !current_sp - n,!current_sp) - in - Cic.AVar - (xid, - (UriManager.uri_of_string - ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var")) - ) - | _ -> raise (IllFormedXml 18) +(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *) + Cic.AVar (xid,uri,[]) end ;; @@ -281,14 +277,15 @@ class eltype_apply = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let children = n#sub_nodes and id = string_of_xml_attr (n#attribute "id") in if List.length children < 2 then raise (IllFormedXml 8) else Cic.AAppl - (id,List.map (fun x -> x#extension#to_cic_term) children) + (id,List.map (fun x -> x#extension#to_cic_term []) children) end ;; @@ -297,7 +294,8 @@ class eltype_cast = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let n = self#node in let sons = n#sub_nodes and id = string_of_xml_attr (n#attribute "id") in @@ -305,8 +303,8 @@ class eltype_cast = [te ; ty] when te#node_type = Pxp_document.T_element "term" && ty#node_type = Pxp_document.T_element "type" -> - let term = te#extension#to_cic_term - and typ = ty#extension#to_cic_term in + let term = te#extension#to_cic_term [] + and typ = ty#extension#to_cic_term [] in Cic.ACast (id,term,typ) | _ -> raise (IllFormedXml 9) end @@ -317,7 +315,8 @@ class eltype_sort = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; 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 @@ -330,12 +329,12 @@ class eltype_const = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in let value = uri_of_xml_attr (n#attribute "uri") and id = string_of_xml_attr (n#attribute "id") in - Cic.AConst (id,value, U.relative_depth !current_uri value 0) + Cic.AConst (id,value, exp_named_subst) end ;; @@ -344,14 +343,14 @@ class eltype_mutind = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in 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 Cic.AMutInd - (id,name, U.relative_depth !current_uri name 0, noType) + (id,name, noType, exp_named_subst) end ;; @@ -360,7 +359,7 @@ class eltype_mutconstruct = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = let module U = UriManager in let n = self#node in let name = uri_of_xml_attr (n#attribute "uri") @@ -368,8 +367,7 @@ class eltype_mutconstruct = and noConstr = int_of_xml_attr (n#attribute "noConstr") and id = string_of_xml_attr (n#attribute "id") in Cic.AMutConstruct - (id, name, U.relative_depth !current_uri name 0, - noType, noConstr) + (id, name, noType, noConstr, exp_named_subst) end ;; @@ -378,19 +376,25 @@ class eltype_prod = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; 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 "source" && - t#node_type = Pxp_document.T_element "target" -> - 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 - Cic.AProd (id,name,source,target) - | _ -> raise (IllFormedXml 10) + let sons = n#sub_nodes in + let rec get_decls_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "decl" -> + let decls,target = get_decls_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::decls, target + | _ -> raise (IllFormedXml 10) + in + let decls,target = get_decls_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.AProd (id,b,s,t)) + decls target end ;; @@ -399,7 +403,8 @@ class eltype_mutcase = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; let module U = UriManager in let n = self#node in let sons = n#sub_nodes @@ -410,12 +415,12 @@ class eltype_mutcase = te#node_type = Pxp_document.T_element "inductiveTerm" -> let ci = uri_of_xml_attr (n#attribute "uriType") and typeno = int_of_xml_attr (n#attribute "noType") - and inductiveType = ty#extension#to_cic_term - and inductiveTerm = te#extension#to_cic_term - and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns + and inductiveType = ty#extension#to_cic_term [] + and inductiveTerm = te#extension#to_cic_term [] + and lpattern = + List.map (fun x -> x#extension#to_cic_term []) patterns in - Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0, - typeno,inductiveType,inductiveTerm,lpattern) + Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern) | _ -> raise (IllFormedXml 11) end ;; @@ -425,19 +430,25 @@ class eltype_lambda = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; 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 "source" && - t#node_type = Pxp_document.T_element "target" -> - 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 - Cic.ALambda (id,name,source,target) - | _ -> raise (IllFormedXml 12) + let sons = n#sub_nodes in + let rec get_decls_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "decl" -> + let decls,target = get_decls_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::decls, target + | _ -> raise (IllFormedXml 12) + in + let decls,target = get_decls_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.ALambda (id,b,s,t)) + decls target end ;; @@ -446,22 +457,64 @@ class eltype_letin = inherit cic_term - method to_cic_term = + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; 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 - Cic.ALetIn (id,name,source,target) - | _ -> raise (IllFormedXml 12) + let sons = n#sub_nodes in + let rec get_defs_and_target = + function + [t] when t#node_type = Pxp_document.T_element "target" -> + [],t#extension#to_cic_term [] + | s::tl when s#node_type = Pxp_document.T_element "def" -> + let defs,target = get_defs_and_target tl in + let id = string_of_xml_attr (s#attribute "id") in + let binder = cic_attr_of_xml_attr (s#attribute "binder") in + (id,binder,s#extension#to_cic_term [])::defs, target + | _ -> raise (IllFormedXml 12) + in + let defs,target = get_defs_and_target sons in + List.fold_right + (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t)) + defs target end ;; +class eltype_instantiate = + object (self) + + inherit cic_term + + method to_cic_term exp_named_subst = + assert (exp_named_subst = []) ; + let n = self#node in +(* CSC: this optional attribute should be parsed and reflected in Cic.annterm + and id = string_of_xml_attr (n#attribute "id") +*) + match n#sub_nodes with + t::l -> + let baseUri = + UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in + let exp_named_subst = + List.map + (function + n when n#node_type = Pxp_document.T_element "arg" -> + let relUri = string_of_xml_attr (n#attribute "relUri") in + let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in + let arg = + match n#sub_nodes with + [ t ] -> t#extension#to_cic_term [] + | _ -> raise (IllFormedXml 7) + in + (uri, arg) + | _ -> raise (IllFormedXml 7) + ) l + in + t#extension#to_cic_term exp_named_subst + | _ -> raise (IllFormedXml 7) + end +;; + + (* The definition of domspec, an hashtable that maps each node type to the *) (* object that must be linked to it. Used by markup. *) @@ -487,11 +540,13 @@ let domspec = "MUTCASE", (new D.element_impl (new eltype_mutcase)) ; "FIX", (new D.element_impl (new eltype_fix)) ; "COFIX", (new D.element_impl (new eltype_cofix)) ; + "instantiate", (new D.element_impl (new eltype_instantiate)) ; "arity", (new D.element_impl (new eltype_transparent)) ; "term", (new D.element_impl (new eltype_transparent)) ; "type", (new D.element_impl (new eltype_transparent)) ; "body", (new D.element_impl (new eltype_transparent)) ; - "source", (new D.element_impl (new eltype_transparent)) ; + "decl", (new D.element_impl (new eltype_transparent)) ; + "def", (new D.element_impl (new eltype_transparent)) ; "target", (new D.element_impl (new eltype_transparent)) ; "letintarget", (new D.element_impl (new eltype_transparent)) ; "patternsType", (new D.element_impl (new eltype_transparent)) ; diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli index 990346e82..c3664c819 100644 --- a/helm/ocaml/cic/cicParser3.mli +++ b/helm/ocaml/cic/cicParser3.mli @@ -56,7 +56,8 @@ class virtual cic_term : (* a method that returns the internal representation of the tree (term) *) (* rooted in this node *) - method virtual to_cic_term : Cic.annterm + method virtual to_cic_term : + (UriManager.uri * Cic.annterm) list -> Cic.annterm end diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index ec98b9774..c27a9d576 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -23,16 +23,16 @@ * http://cs.unibo.it/helm/. *) -let expect_possible_parameters = ref false;; - -exception NotExpectingPossibleParameters;; - (* converts annotated terms into cic terms (forgetting ids and names) *) let rec deannotate_term = let module C = Cic in function - C.ARel (_,n,_) -> C.Rel n - | C.AVar (_,uri) -> C.Var uri + C.ARel (_,_,n,_) -> C.Rel n + | C.AVar (_,uri,exp_named_subst) -> + let deann_exp_named_subst = + List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst + in + C.Var (uri, deann_exp_named_subst) | C.AMeta (_,n, l) -> let l' = List.map @@ -52,50 +52,53 @@ let rec deannotate_term = | 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.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.MutCase (uri,cookingsno,i,deannotate_term outtype, + | C.AConst (_,uri,exp_named_subst) -> + let deann_exp_named_subst = + List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst + in + C.Const (uri, deann_exp_named_subst) + | C.AMutInd (_,uri,i,exp_named_subst) -> + let deann_exp_named_subst = + List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst + in + C.MutInd (uri,i,deann_exp_named_subst) + | C.AMutConstruct (_,uri,i,j,exp_named_subst) -> + let deann_exp_named_subst = + List.map (function (uri,t) -> uri,deannotate_term t) exp_named_subst + in + C.MutConstruct (uri,i,j,deann_exp_named_subst) + | C.AMutCase (_,uri,i,outtype,te,pl) -> + C.MutCase (uri,i,deannotate_term outtype, deannotate_term te, List.map deannotate_term pl) | C.AFix (_,funno,ifl) -> C.Fix (funno, List.map deannotate_inductiveFun ifl) | C.ACoFix (_,funno,ifl) -> C.CoFix (funno, List.map deannotate_coinductiveFun ifl) -and deannotate_inductiveFun (name,index,ty,bo) = +and deannotate_inductiveFun (_,name,index,ty,bo) = (name, index, deannotate_term ty, deannotate_term bo) -and deannotate_coinductiveFun (name,ty,bo) = +and deannotate_coinductiveFun (_,name,ty,bo) = (name, deannotate_term ty, deannotate_term bo) ;; let deannotate_inductiveType (name, isinductive, arity, cons) = (name, isinductive, deannotate_term arity, - List.map (fun (id,ty,recs) -> (id,deannotate_term ty, recs)) cons) + List.map (fun (id,ty) -> (id,deannotate_term ty)) cons) ;; let deannotate_obj = let module C = Cic in function - C.ADefinition (_, id, bo, ty, params) -> - (match params with - C.Possible params -> - if !expect_possible_parameters then - C.Definition (id, deannotate_term bo, deannotate_term ty, params) - else - raise NotExpectingPossibleParameters - | C.Actual params -> - C.Definition (id, deannotate_term bo, deannotate_term ty, params) - ) - | C.AAxiom (_, id, ty, params) -> - C.Axiom (id, deannotate_term ty, params) - | C.AVariable (_, name, bo, ty) -> + C.AConstant (_, _, id, bo, ty, params) -> + C.Constant (id, + (match bo with None -> None | Some bo -> Some (deannotate_term bo)), + deannotate_term ty, params) + | C.AVariable (_, name, bo, ty, params) -> C.Variable (name, (match bo with None -> None | Some bo -> Some (deannotate_term bo)), - deannotate_term ty) - | C.ACurrentProof (_, name, conjs, bo, ty) -> + deannotate_term ty, params) + | C.ACurrentProof (_, _, name, conjs, bo, ty, params) -> C.CurrentProof ( name, List.map @@ -113,7 +116,7 @@ let deannotate_obj = in (id,context,deannotate_term con) ) conjs, - deannotate_term bo,deannotate_term ty + deannotate_term bo,deannotate_term ty,params ) | C.AInductiveDefinition (_, tys, params, parno) -> C.InductiveDefinition ( List.map deannotate_inductiveType tys, diff --git a/helm/ocaml/cic/deannotate.mli b/helm/ocaml/cic/deannotate.mli index d1bd72c07..89b18d2d6 100644 --- a/helm/ocaml/cic/deannotate.mli +++ b/helm/ocaml/cic/deannotate.mli @@ -32,8 +32,5 @@ (* *) (******************************************************************************) -(* Useful only for fix_params *) -val expect_possible_parameters : bool ref - val deannotate_term : Cic.annterm -> Cic.term val deannotate_obj : Cic.annobj -> Cic.obj diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index 1961a2bc2..bffa4b0fc 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -50,8 +50,7 @@ let print_term i2a = let module X = Xml in let module U = UriManager in function - C.ARel (id,_,_) -> print_ann i2a id - | C.AVar (id,_) -> print_ann i2a id + C.ARel (id,_,_,_) -> print_ann i2a id | C.AMeta (id,_,_) -> print_ann i2a id | C.ASort (id,_) -> print_ann i2a id | C.AImplicit _ -> raise NotImplemented @@ -63,10 +62,16 @@ let print_term i2a = [< print_ann i2a id ; List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>] >] - | C.AConst (id,_,_) -> print_ann i2a id - | C.AMutInd (id,_,_,_) -> print_ann i2a id - | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id - | C.AMutCase (id,_,_,_,ty,te,patterns) -> + | C.AVar (id,_,exp_named_subst) + | C.AConst (id,_,exp_named_subst) + | C.AMutInd (id,_,_,exp_named_subst) + | C.AMutConstruct (id,_,_,_,exp_named_subst) -> + [< print_ann i2a id ; + List.fold_right + (fun (_,x) i -> [< aux x ; i >]) + exp_named_subst [<>] + >] + | C.AMutCase (id,_,_,ty,te,patterns) -> [< print_ann i2a id ; aux ty ; aux te ; @@ -77,12 +82,12 @@ let print_term i2a = | C.AFix (id,_,funs) -> [< print_ann i2a id ; List.fold_right - (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] + (fun (_,_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] >] | C.ACoFix (id,no,funs) -> [< print_ann i2a id ; List.fold_right - (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] + (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] >] in aux @@ -91,7 +96,7 @@ let print_term i2a = let print_mutual_inductive_type i2a (_,_,arity,constructors) = [< print_term i2a arity ; List.fold_right - (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>] + (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>] >] ;; @@ -104,10 +109,19 @@ let pp_annotation obj i2a curi = ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] begin match obj with - 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) -> + C.AConstant (xid, xidobj, _, te, ty, _) -> + [< print_ann i2a xid ; + (match xidobj,te with + Some xidobj, Some te -> + [< print_ann i2a xidobj ; + print_term i2a te + >] + | None, None -> [<>] + | _,_ -> assert false + ) ; + print_term i2a ty + >] + | C.AVariable (xid, _, bo, ty,_) -> [< print_ann i2a xid ; (match bo with None -> [<>] @@ -115,8 +129,9 @@ let pp_annotation obj i2a curi = ) ; print_term i2a ty >] - | C.ACurrentProof (xid, _, conjs, bo, ty) -> + | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) -> [< print_ann i2a xid ; + print_ann i2a xidobj ; List.fold_right (fun (cid, _, context, t) i -> [< print_ann i2a cid ; diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.ml b/helm/ocaml/cic_annotations/cicAnnotationParser.ml index 7b4fdad6a..d8c67ea63 100644 --- a/helm/ocaml/cic_annotations/cicAnnotationParser.ml +++ b/helm/ocaml/cic_annotations/cicAnnotationParser.ml @@ -41,9 +41,7 @@ let get_annotations filename = let d = let config = {Y.default_config with Y.warner = new warner} in Y.parse_document_entity config -(*PXP (Y.ExtID (Pxp_types.System filename, - new Pxp_reader.resolve_as_file ~url_of_id ())) -*) (PxpUriResolver.from_file filename) + (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) Y.default_spec in diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml index f2cb0ed40..14ba1da50 100644 --- a/helm/ocaml/cic_annotations/cicXPath.ml +++ b/helm/ocaml/cic_annotations/cicXPath.ml @@ -56,8 +56,7 @@ let get_ids_to_targets annobj = in let rec add_target_term t = match t with - C.ARel (id,_,_) - | C.AVar (id,_) + C.ARel (id,_,_,_) | C.AMeta (id,_,_) | C.ASort (id,_) | C.AImplicit id -> @@ -75,46 +74,52 @@ let get_ids_to_targets annobj = | C.AAppl (id,l) -> set_target id (C.Term t) ; List.iter add_target_term l - | C.AConst (id,_,_) - | C.AMutInd (id,_,_,_) - | C.AMutConstruct (id,_,_,_,_) -> - set_target id (C.Term t) - | C.AMutCase (id,_,_,_,ot,it,pl) -> + | C.AVar (id,_,exp_named_subst) + | C.AConst (id,_,exp_named_subst) + | C.AMutInd (id,_,_,exp_named_subst) + | C.AMutConstruct (id,_,_,_,exp_named_subst) -> + set_target id (C.Term t) ; + List.iter (function (_,t) -> add_target_term t) exp_named_subst + | 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) -> + (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) -> + (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,_) -> + C.AConstant (id,idbody,_,bo,ty,_) -> set_target id (C.Object annobj) ; + (match idbody,bo with + Some idbody,Some bo -> + set_target idbody (C.ConstantBody annobj) ; + add_target_term bo + | None, None -> () + | _,_ -> assert false + ) ; add_target_term ty - | C.AVariable (id,_,None,ty) -> + | C.AVariable (id,_,None,ty,_) -> set_target id (C.Object annobj) ; add_target_term ty - | C.AVariable (id,_,Some bo,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) -> + | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) -> set_target id (C.Object annobj) ; + set_target idbody (C.ConstantBody annobj) ; List.iter (function (cid,_,context, t) as annconj -> set_target cid (C.Conjecture annconj) ; List.iter @@ -133,7 +138,7 @@ let get_ids_to_targets annobj = List.iter (function (_,_,arity,cl) -> add_target_term arity ; - List.iter (function (_,ty,_) -> add_target_term ty) cl + List.iter (function (_,ty) -> add_target_term ty) cl ) itl in add_target_obj annobj ; diff --git a/helm/ocaml/cic_annotations_cache/cicCache.ml b/helm/ocaml/cic_annotations_cache/cicCache.ml index 8bc4be6c4..58a8f4197 100644 --- a/helm/ocaml/cic_annotations_cache/cicCache.ml +++ b/helm/ocaml/cic_annotations_cache/cicCache.ml @@ -39,7 +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 - let annobj = CicParser.annobj_of_xml cicfilename uri in + let cicbodyfilename = + match U.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + Some (G.getxml (U.cicuri_of_uri bodyuri)) + in + let annobj = CicParser.annobj_of_xml cicfilename cicbodyfilename uri in annobj, if U.uri_is_annuri uri then begin diff --git a/helm/ocaml/cic_cache/cicCache.ml b/helm/ocaml/cic_cache/cicCache.ml index adfeb0575..71fc4e638 100644 --- a/helm/ocaml/cic_cache/cicCache.ml +++ b/helm/ocaml/cic_cache/cicCache.ml @@ -39,12 +39,22 @@ let get_annobj uri = let module G = Getter in let module U = UriManager in let cicfilename = G.getxml (U.cicuri_of_uri uri) in - CicParser.annobj_of_xml cicfilename uri + match (U.bodyuri_of_uri uri) with + None -> + CicParser.annobj_of_xml cicfilename None uri + | Some bodyuri -> + let cicbodyfilename = G.getxml (U.cicuri_of_uri bodyuri) in + CicParser.annobj_of_xml cicfilename (Some cicbodyfilename) uri ;; let get_obj 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 + match (U.bodyuri_of_uri uri) with + None -> + CicParser.obj_of_xml cicfilename None uri + | Some bodyuri -> + let cicbodyfilename = G.getxml (U.cicuri_of_uri bodyuri) in + CicParser.obj_of_xml cicfilename (Some cicbodyfilename) uri ;; diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 04373b39e..65f5443ab 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -1,13 +1,17 @@ -cicSubstitution.cmo: cicSubstitution.cmi -cicSubstitution.cmx: cicSubstitution.cmi logger.cmo: logger.cmi logger.cmx: logger.cmi -cicEnvironment.cmo: cicSubstitution.cmi cicEnvironment.cmi -cicEnvironment.cmx: cicSubstitution.cmx cicEnvironment.cmi +cicEnvironment.cmo: cicEnvironment.cmi +cicEnvironment.cmx: cicEnvironment.cmi cicPp.cmo: cicEnvironment.cmi cicPp.cmi cicPp.cmx: cicEnvironment.cmx cicPp.cmi +cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi +cicSubstitution.cmx: cicEnvironment.cmx cicSubstitution.cmi cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi +cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ + cicReductionNaif.cmi +cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ + cicReductionNaif.cmi cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ cicReduction.cmi cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ @@ -16,5 +20,3 @@ cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \ cicSubstitution.cmi logger.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ cicSubstitution.cmx logger.cmx cicTypeChecker.cmi -cicCooking.cmo: cicEnvironment.cmi cicCooking.cmi -cicCooking.cmx: cicEnvironment.cmx cicCooking.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index b4e5b8ae6..95ce4ad15 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -2,9 +2,9 @@ PACKAGE = cic_proof_checking REQUIRES = helm-cic PREDICATES = -INTERFACE_FILES = cicSubstitution.mli logger.mli cicEnvironment.mli cicPp.mli \ - cicMiniReduction.mli cicReduction.mli cicTypeChecker.mli \ - cicCooking.mli +INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ + cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ + cicTypeChecker.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 9d93c443e..7ed957271 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -35,18 +35,17 @@ (* *) (******************************************************************************) +let cleanup_tmp = true;; + +let never_trust = function uri -> false;; +let always_trust = function uri -> true;; +let trust_obj = ref never_trust;; + type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj to proof-check *) ;; -exception NoFunctionProvided;; - -let cook_obj = ref (fun obj uri -> raise NoFunctionProvided);; - -let set_cooking_function foo = - cook_obj := foo -;; exception AlreadyCooked of string;; exception CircularDependency of string;; @@ -62,22 +61,16 @@ module Cache : UriManager.uri -> get_object_to_add:(unit -> Cic.obj) -> Cic.obj val unchecked_to_frozen : UriManager.uri -> unit val frozen_to_cooked : - uri:UriManager.uri -> - cooking_procedure: - (object_to_cook:Cic.obj -> - add_cooked:(UriManager.uri * int-> Cic.obj -> unit) - -> unit - ) - -> unit - val find_cooked : key:(UriManager.uri * int) -> Cic.obj + uri:UriManager.uri -> unit + val find_cooked : key:UriManager.uri -> Cic.obj end = struct module CacheOfCookedObjects : sig - val mem : UriManager.uri -> int -> bool - val find : UriManager.uri -> int -> Cic.obj - val add : UriManager.uri -> int -> Cic.obj -> unit + val mem : UriManager.uri -> bool + val find : UriManager.uri -> Cic.obj + val add : UriManager.uri -> Cic.obj -> unit end = struct @@ -90,29 +83,16 @@ module Cache : ;; module HT = Hashtbl.Make(HashedType);; let hashtable = HT.create 1009;; - let mem uri cookingsno = + let mem uri = try - let cooked_list = - HT.find hashtable uri - in - List.mem_assq cookingsno !cooked_list + HT.mem hashtable uri with Not_found -> false ;; - let find uri cookingsno = - List.assq cookingsno !(HT.find hashtable uri) + let find uri = HT.find hashtable uri ;; - let add uri cookingsno obj = - let cooked_list = - try - HT.find hashtable uri - with - Not_found -> - let newl = ref [] in - HT.add hashtable uri newl ; - newl - in - cooked_list := (cookingsno,obj)::!cooked_list + let add uri obj = + HT.add hashtable uri obj ;; end ;; @@ -127,7 +107,7 @@ module Cache : if List.mem_assq uri !frozen_list then raise (CircularDependency (UriManager.string_of_uri uri)) else - if CacheOfCookedObjects.mem uri 0 then + if CacheOfCookedObjects.mem uri then raise (AlreadyCooked (UriManager.string_of_uri uri)) else (* OK, it is not already frozen nor cooked *) @@ -143,48 +123,55 @@ module Cache : with Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri)) ;; - let frozen_to_cooked ~uri ~cooking_procedure = + let frozen_to_cooked ~uri = try let obj = List.assq uri !frozen_list in frozen_list := List.remove_assq uri !frozen_list ; - cooking_procedure - ~object_to_cook:obj - ~add_cooked:(fun (uri,cookno) -> CacheOfCookedObjects.add uri cookno) + CacheOfCookedObjects.add uri obj with Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) ;; - let find_cooked ~key:(uri,cookingsno)= CacheOfCookedObjects.find uri cookingsno;; + let find_cooked ~key:uri = CacheOfCookedObjects.find uri;; end ;; -(* get_cooked_obj uri *) -(* returns the cooked cic object whose uri is uri. The term must be present *) -(* and cooked in cache *) -let get_cooked_obj uri cookingsno = - Cache.find_cooked (uri,cookingsno) -;; - let find_or_add_unchecked_to_cache uri = Cache.find_or_add_unchecked uri ~get_object_to_add: (function () -> let filename = Getter.getxml uri in - let obj = CicParser.obj_of_xml filename uri in + let bodyfilename = + match UriManager.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + try + ignore (Getter.resolve bodyuri) ; + (* The body exists ==> it is not an axiom *) + Some (Getter.getxml bodyuri) + with + Getter.Unresolved -> + (* The body does not exist ==> we consider it an axiom *) + None + in + let obj = CicParser.obj_of_xml filename bodyfilename uri in + if cleanup_tmp then + begin + Unix.unlink filename ; + match bodyfilename with + Some f -> Unix.unlink f + | None -> () + end ; obj ) ;; -(* 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 *) -(* the result of Getter.getxml uri *) -let get_obj uri = - try - get_cooked_obj uri 0 - with - Not_found -> - find_or_add_unchecked_to_cache uri -;; +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed *) +let set_type_checking_info uri = + trust_obj := never_trust ; + Cache.frozen_to_cooked uri +;; (* is_type_checked uri *) (* CSC: commento falso ed obsoleto *) @@ -192,39 +179,49 @@ let get_obj uri = (* otherwise it freezes the term for type-checking and returns it *) (* set_type_checking_info must be called to unfreeze the term *) -let is_type_checked uri cookingsno = +let is_type_checked uri = try - CheckedObj (Cache.find_cooked (uri,cookingsno)) + CheckedObj (Cache.find_cooked uri) with Not_found -> let obj = find_or_add_unchecked_to_cache uri in Cache.unchecked_to_frozen uri ; - UncheckedObj obj + if !trust_obj uri then + begin +prerr_endline ("### " ^ UriManager.string_of_uri uri ^ " TRUSTED!!!") ; + set_type_checking_info uri ; + trust_obj := always_trust ; + CheckedObj (Cache.find_cooked uri) + end + else + begin + trust_obj := always_trust ; + UncheckedObj obj + end ;; -(* set_type_checking_info uri *) -(* must be called once the type-checking of uri is finished *) -(* The object whose uri is uri is unfreezed *) -let set_type_checking_info uri = - Cache.frozen_to_cooked uri - (fun ~object_to_cook:obj ~add_cooked -> - (* let's cook the object at every level *) - let obj' = CicSubstitution.undebrujin_inductive_def uri obj in - add_cooked (uri,0) obj' ; - let cooked_objs = !cook_obj obj' uri in - let last_cooked_level = ref 0 in - let last_cooked_obj = ref obj' in - List.iter - (fun (n,cobj) -> - for i = !last_cooked_level + 1 to n do - add_cooked (uri,i) !last_cooked_obj - done ; - add_cooked (uri,n + 1) cobj ; - last_cooked_level := n + 1 ; - last_cooked_obj := cobj - ) cooked_objs ; - for i = !last_cooked_level + 1 to UriManager.depth_of_uri uri + 1 do - add_cooked (uri,i) !last_cooked_obj - done - ) +(* get_cooked_obj uri *) +(* returns the cooked cic object whose uri is uri. The term must be present *) +(* and cooked in cache *) +let get_cooked_obj uri = + try + Cache.find_cooked uri + with Not_found -> + if not (!trust_obj uri) then + prerr_endline ("@@@ OOOOOOOPS: WE TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE SHOULD NOT DO THAT! THAT MEANS LOOKING FOR TROUBLES ;-(") ; + match is_type_checked uri with + CheckedObj obj -> obj + | _ -> assert false ;; + +(* 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 *) +(* the result of Getter.getxml uri *) +let get_obj uri = + try + get_cooked_obj uri + with + Not_found -> + find_or_add_unchecked_to_cache uri +;; diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 22fd5d657..c54df77e2 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -53,7 +53,7 @@ type type_checked_obj = (* otherwise it returns (false,object) and freeze the object for *) (* type-checking *) (* set_type_checking_info must be called to unfreeze the object *) -val is_type_checked : UriManager.uri -> int -> type_checked_obj +val is_type_checked : UriManager.uri -> type_checked_obj (* set_type_checking_info uri *) (* must be called once the type-checking of uri is finished *) @@ -61,9 +61,5 @@ val is_type_checked : UriManager.uri -> int -> type_checked_obj (* again in the future (is_type_checked will return true) *) val set_type_checking_info : UriManager.uri -> unit -(* get_cooked_obj uri cookingsno *) -val get_cooked_obj : UriManager.uri -> int -> Cic.obj - -(* set_cooking_function cooking_function *) -val set_cooking_function : - (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit +(* get_cooked_obj uri *) +val get_cooked_obj : UriManager.uri -> Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml index bdc6e3a09..1f6b72636 100644 --- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml @@ -27,7 +27,11 @@ let rec letin_nf = let module C = Cic in function C.Rel _ as t -> t - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst + in + C.Var (uri,exp_named_subst') | C.Meta _ as t -> t | C.Sort _ as t -> t | C.Implicit as t -> t @@ -36,12 +40,23 @@ let rec letin_nf = | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t) | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t | C.Appl l -> C.Appl (List.map letin_nf l) - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t, - List.map letin_nf pl) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,letin_nf outt, letin_nf t, List.map letin_nf pl) | C.Fix (i,fl) -> let substitutedfl = List.map diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index fce4e7f48..05c964370 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -44,7 +44,7 @@ exception NotEnoughElements;; let string_of_name = function Cic.Name s -> s - | Cic.Anonimous -> "_" + | Cic.Anonymous -> "_" ;; (* get_nth l n returns the nth element of the list l if it exists or *) @@ -68,12 +68,14 @@ let rec pp t l = try (match get_nth l n with Some (C.Name s) -> s - | _ -> raise CicPpInternalError + | Some C.Anonymous -> "__" ^ string_of_int n + | _ -> raise CicPpInternalError ) with NotEnoughElements -> string_of_int (List.length l - n) end - | C.Var uri -> UriManager.name_of_uri uri + | C.Var (uri,exp_named_subst) -> + UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l | C.Meta (n,l1) -> "?" ^ (string_of_int n) ^ "[" ^ String.concat " ; " @@ -89,7 +91,7 @@ let rec pp t l = | C.Prod (b,s,t) -> (match b with C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) - | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" + | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" ) | C.Cast (v,t) -> pp v l | C.Lambda (b,s,t) -> @@ -102,41 +104,29 @@ let rec pp t l = (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i) li "" ) ^ ")" - | C.Const (uri,_) -> UriManager.name_of_uri uri - | C.MutInd (uri,_,n) -> - begin - try - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> - let (name,_,_,_) = get_nth dl (n+1) in - name - | _ -> raise CicPpInternalError - ) - with - NotEnoughElements -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1) - end - | C.MutConstruct (uri,_,n1,n2) -> - begin - try - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> - let (_,_,_,cons) = get_nth dl (n1+1) in - let (id,_,_) = get_nth cons n2 in - id - | _ -> raise CicPpInternalError - ) - with - NotEnoughElements -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^ - string_of_int n2 - end - | C.MutCase (uri,_,n1,ty,te,patterns) -> + | C.Const (uri,exp_named_subst) -> + UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l + | C.MutInd (uri,n,exp_named_subst) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + name ^ pp_exp_named_subst exp_named_subst l + | _ -> raise CicPpInternalError + ) + | C.MutConstruct (uri,n1,n2,exp_named_subst) -> + (match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + let (id,_) = get_nth cons n2 in + id ^ pp_exp_named_subst exp_named_subst l + | _ -> raise CicPpInternalError + ) + | C.MutCase (uri,n1,ty,te,patterns) -> let connames = (match CicEnvironment.get_obj uri with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in - List.map (fun (id,_,_) -> id) cons + List.map (fun (id,_) -> id) cons | _ -> raise CicPpInternalError ) in @@ -168,6 +158,14 @@ let rec pp t l = pp bo (names@l) ^ i) funs "" ^ "}\n" +and pp_exp_named_subst exp_named_subst l = + if exp_named_subst = [] then "" else + "{" ^ + String.concat " ; " ( + List.map + (function (uri,t) -> UriManager.name_of_uri uri ^ ":=" ^ pp t l) + exp_named_subst + ) ^ "}" ;; let ppterm t = @@ -185,7 +183,7 @@ let ppinductiveType (typename, inductive, arity, cons) names = (*CSC: bug found: was pp arity names ^ " =\n " ^*) pp arity [] ^ " =\n " ^ List.fold_right - (fun (id,ty,_) i -> id ^ " : " ^ pp ty names ^ + (fun (id,ty) i -> id ^ " : " ^ pp ty names ^ (if i = "" then "\n" else "\n | ") ^ i) cons "" ;; @@ -196,32 +194,24 @@ let ppobj obj = let module C = Cic in let module U = UriManager in match obj with - C.Definition (id, t1, t2, params) -> - "Definition of " ^ id ^ - "(" ^ - List.fold_right - (fun (_,x) i -> - List.fold_right - (fun x i -> - U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' - ) x "" ^ match i with "" -> "" | i' -> " " ^ i' - ) params "" ^ ")" ^ - ":\n" ^ pp t1 [] ^ " : " ^ pp t2 [] - | C.Axiom (id, ty, params) -> - "Axiom " ^ id ^ "(" ^ - List.fold_right - (fun (_,x) i -> - List.fold_right - (fun x i -> - U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' - ) x "" ^ match i with "" -> "" | i' -> " " ^ i' - ) params "" ^ - "):\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" ^ + C.Constant (name, Some t1, t2, params) -> + "Definition of " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 [] + | C.Constant (name, None, ty, params) -> + "Axiom " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + "):\n" ^ pp ty [] + | C.Variable (name, bo, ty, params) -> + "Variable " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ + pp ty [] ^ "\n" ^ + (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) + | C.CurrentProof (name, conjectures, value, ty, params) -> + "Current Proof of " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ let separate s = if s = "" then "" else s ^ " ; " in List.fold_right (fun (n, context, t) i -> @@ -247,14 +237,8 @@ let ppobj obj = "\n" ^ pp value [] ^ " : " ^ pp ty [] | C.InductiveDefinition (l, params, nparams) -> "Parameters = " ^ - List.fold_right - (fun (_,x) i -> - List.fold_right - (fun x i -> - U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i' - ) x "" ^ match i with "" -> "" | i' -> " " ^ i' - ) params "" ^ "\n" ^ - "NParams = " ^ string_of_int nparams ^ "\n" ^ - let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in - List.fold_right (fun x i -> ppinductiveType x names ^ i) l "" + String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^ + "NParams = " ^ string_of_int nparams ^ "\n" ^ + let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in + List.fold_right (fun x i -> ppinductiveType x names ^ i) l "" ;; diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli index c4332a2ed..7a6255003 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.mli +++ b/helm/ocaml/cic_proof_checking/cicReduction.mli @@ -24,8 +24,7 @@ *) exception WrongUriToInductiveDefinition -exception ReferenceToDefinition -exception ReferenceToAxiom +exception ReferenceToConstant exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 93335625a..e45702077 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -25,13 +25,18 @@ exception CicReductionInternalError;; exception WrongUriToInductiveDefinition;; +exception Impossible of int;; +exception ReferenceToConstant;; +exception ReferenceToVariable;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; let fdebug = ref 1;; 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, t)) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i in if !fdebug = 0 then begin @@ -40,269 +45,427 @@ let debug t env s = end ;; -exception Impossible of int;; -exception ReferenceToDefinition;; -exception ReferenceToAxiom;; -exception ReferenceToVariable;; -exception ReferenceToCurrentProof;; -exception ReferenceToInductiveDefinition;; - type env = Cic.term list;; type stack = Cic.term list;; -type config = int * env * Cic.term * stack;; +type config = + int * env * Cic.term Cic.explicit_named_substitution * Cic.term * stack;; + +let lazily = true;; (* k is the length of the environment e *) (* m is the current depth inside the term *) -let unwind' m k e t = - let module C = Cic in - let module S = CicSubstitution in - if e = [] & k = 0 then t else - let rec unwind_aux m = function - C.Rel n as t -> if n <= m then t else - let d = try Some (List.nth e (n-m-1)) - with _ -> None - in (match d with - Some t' -> if m = 0 then t' - else S.lift m t' - | None -> C.Rel (n-k)) - | C.Var _ as t -> t - | C.Meta (i,l) as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *) - | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.Appl l -> C.Appl (List.map (unwind_aux m) l) - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,unwind_aux m outt, unwind_aux m t, - List.map (unwind_aux m) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, unwind_aux m ty, unwind_aux (m+len) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let len = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo)) - fl - in - C.CoFix (i, substitutedfl) - in - unwind_aux m t - ;; +let unwind' m k e ens t = + let module C = Cic in + let module S = CicSubstitution in + if k = 0 && ens = [] then + t + else + let rec unwind_aux m = + function + C.Rel n as t -> + if n <= m then t else + let d = + try + Some (List.nth e (n-m-1)) + with _ -> None + in + (match d with + Some t' -> + if m = 0 then t' else S.lift m t' + | None -> C.Rel (n-k) + ) + | C.Var (uri,exp_named_subst) -> +(* +prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ; +*) + if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then + CicSubstitution.lift m (List.assq uri ens) + else + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable (_,_,_,params) -> params + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in + let exp_named_subst' = + substaux_in_exp_named_subst params exp_named_subst m + in + C.Var (uri,exp_named_subst') + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (unwind_aux m t) + ) l + in + C.Meta (i, l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ??? *) + | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.Appl l -> C.Appl (List.map (unwind_aux m) l) + | C.Const (uri,exp_named_subst) -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant (_,_,_,params) -> params + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,_,_,params) -> params + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in + let exp_named_subst' = + substaux_in_exp_named_subst params exp_named_subst m + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition (_,params,_) -> params + ) + in + let exp_named_subst' = + substaux_in_exp_named_subst params exp_named_subst m + in + C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition (_,params,_) -> params + ) + in + let exp_named_subst' = + substaux_in_exp_named_subst params exp_named_subst m + in + C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t, + List.map (unwind_aux m) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> + (name, i, unwind_aux m ty, unwind_aux (m+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + and substaux_in_exp_named_subst params exp_named_subst' m = +(*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params + let ens' = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ +(*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) + List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens + in + let rec filter_and_lift = + function + [] -> [] + | uri::tl -> + let r = filter_and_lift tl in + (try + (uri,(List.assq uri ens'))::r + with + Not_found -> r + ) + in + filter_and_lift params +*) + +(*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) +(*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) + +(*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) +(*CSC: codice altamente inefficiente *) + let rec filter_and_lift already_instantiated = + function + [] -> [] + | (uri,t)::tl when + List.for_all + (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' + && + not (List.mem uri already_instantiated) + && + List.mem uri params + -> + (uri,CicSubstitution.lift m t) :: + (filter_and_lift (uri::already_instantiated) tl) + | _::tl -> filter_and_lift already_instantiated tl +(* + | (uri,_)::tl -> +prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ; +if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ; +prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ; +if List.mem uri params then prerr_endline "---- OK2" ; + filter_and_lift tl +*) + in + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + unwind_aux m t +;; let unwind = unwind' 0 ;; -let rec reduce : config -> Cic.term = - let module C = Cic in - let module S = CicSubstitution in - function - (k, e, (C.Rel n as t), s) -> let d = -(* prerr_string ("Rel " ^ string_of_int n) ; flush stderr ; *) - try Some (List.nth e (n-1)) - with _ -> None - in (match d with - Some t' -> reduce (0, [],t',s) - | None -> if s = [] then C.Rel (n-k) - else C.Appl (C.Rel (n-k)::s)) - | (k, e, (C.Var uri as t), s) -> - (match CicEnvironment.get_cooked_obj uri 0 with - C.Definition _ -> raise ReferenceToDefinition - | C.Axiom _ -> raise ReferenceToAxiom +let reduce context : config -> Cic.term = + let module C = Cic in + let module S = CicSubstitution in + let rec reduce = + function + (k, e, _, (C.Rel n as t), s) -> + let d = + try + Some (List.nth e (n-1)) + with + _ -> + try + begin + match List.nth context (n - 1 - k) with + None -> assert false + | Some (_,C.Decl _) -> None + | Some (_,C.Def x) -> Some (S.lift (n - k) x) + end + with + _ -> None + in + (match d with + Some t' -> reduce (0,[],[],t',s) + | None -> + if s = [] then + C.Rel (n-k) + else C.Appl (C.Rel (n-k)::s) + ) + | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) -> + if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then + reduce (0, [], [], List.assq uri ens, s) + else + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_) -> if s = [] then t else C.Appl (t::s) - | C.Variable (_,Some body,_) -> reduce (0, [], body, s) - ) - | (k, e, (C.Meta _ as t), s) -> if s = [] then t - else C.Appl (t::s) - | (k, e, (C.Sort _ as t), s) -> t (* s should be empty *) - | (k, e, (C.Implicit as t), s) -> t (* s should be empty *) - | (k, e, (C.Cast (te,ty) as t), s) -> reduce (k, e,te,s) (* s should be empty *) - | (k, e, (C.Prod _ as t), s) -> unwind k e t (* s should be empty *) - | (k, e, (C.Lambda (_,_,t) as t'), []) -> unwind k e t' - | (k, e, C.Lambda (_,_,t), p::s) -> -(* prerr_string ("Lambda body: " ^ CicPp.ppterm t) ; flush stderr ; *) - reduce (k+1, p::e,t,s) - | (k, e, (C.LetIn (_,m,t) as t'), s) -> let m' = reduce (k,e,m,[]) in - reduce (k+1, m'::e,t,s) - | (k, e, C.Appl [], s) -> raise (Impossible 1) - (* this is lazy - | (k, e, C.Appl (he::tl), s) -> let tl' = List.map (unwind k e) tl - in reduce (k, e, he, (List.append tl' s)) *) - (* this is strict *) - | (k, e, C.Appl (he::tl), s) -> - (* constants are NOT unfolded *) - let red = function - C.Const _ as t -> t - | t -> reduce (k, e,t,[]) in - let tl' = List.map red tl in - reduce (k, e, he , List.append tl' s) + | C.Variable (_,None,_,_) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + | C.Variable (_,Some body,_,_) -> + let ens' = push_exp_named_subst k e ens exp_named_subst in + reduce (0, [], ens', body, s) + ) + | (k, e, ens, (C.Meta _ as t), s) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) + | (k, e, _, (C.Implicit as t), s) -> t (* s should be empty *) + | (k, e, ens, (C.Cast (te,ty) as t), s) -> + reduce (k, e, ens, te, s) (* s should be empty *) + | (k, e, ens, (C.Prod _ as t), s) -> unwind k e ens t (* s should be empty *) + | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' + | (k, e, ens, C.Lambda (_,_,t), p::s) -> + reduce (k+1, p::e, ens, t,s) + (* lazy *) + | (k, e, ens, (C.LetIn (_,m,t) as t'), s) when lazily -> + let m' = unwind k e ens m in reduce (k+1, m'::e, ens, t, s) + (* strict *) + | (k, e, ens, (C.LetIn (_,m,t) as t'), s) -> + let m' = reduce (k,e,ens,m,[]) in reduce (k+1,m'::e,ens,t,s) + | (_, _, _, C.Appl [], _) -> raise (Impossible 1) + (* lazy *) + | (k, e, ens, C.Appl (he::tl), s) when lazily -> + let tl' = List.map (unwind k e ens) tl in + reduce (k, e, ens, he, (List.append tl' s)) + (* strict, but constants are NOT unfolded *) + | (k, e, ens, C.Appl (he::tl), s) -> + (* constants are NOT unfolded *) + let red = + function + C.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + in + let tl' = List.map red tl in + reduce (k, e, ens, he , List.append tl' s) (* - | (k, e, C.Appl ((C.Lambda _ as he)::tl), s) - | (k, e, C.Appl ((C.Const _ as he)::tl), s) - | (k, e, C.Appl ((C.MutCase _ as he)::tl), s) - | (k, e, C.Appl ((C.Fix _ as he)::tl), s) -> -(* strict evaluation, but constants are NOT - unfolded *) - let red = function - C.Const _ as t -> t - | t -> reduce (k, e,t,[]) in - let tl' = List.map red tl in - reduce (k, e, he , List.append tl' s) - | (k, e, C.Appl l, s) -> C.Appl (List.append (List.map (unwind k e) l) s) *) - | (k, e, (C.Const (uri,cookingsno) as t), s) -> - (match CicEnvironment.get_cooked_obj uri cookingsno with - C.Definition (_,body,_,_) -> reduce (0, [], body, s) - (* constants are closed *) - | C.Axiom _ -> if s = [] then t else C.Appl (t::s) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s) - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s) - | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) -> - let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s) - | (k, e, (C.MutCase (mutind,cookingsno,i,_,term,pl) as t),s) -> - let decofix = - function - C.CoFix (i,fl) as t -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - reduce (0,[],body',[]) - | C.Appl (C.CoFix (i,fl) :: tl) -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body + | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s) + | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s) + | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s) + | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) -> +(* strict evaluation, but constants are NOT unfolded *) + let red = + function + C.Const _ as t -> unwind k e ens t + | t -> reduce (k,e,ens,t,[]) + in + let tl' = List.map red tl in + reduce (k, e, ens, he , List.append tl' s) + | (k, e, ens, C.Appl l, s) -> + C.Appl (List.append (List.map (unwind k e ens) l) s) +*) + | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> + (match CicEnvironment.get_cooked_obj uri with + C.Constant (_,Some body,_,_) -> + let ens' = push_exp_named_subst k e ens exp_named_subst in + (* constants are closed *) + reduce (0, [], ens', body, s) + | C.Constant (_,None,_,_) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,body,_,_) -> + let ens' = push_exp_named_subst k e ens exp_named_subst in + (* constants are closed *) + reduce (0, [], ens', body, s) + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + | (k, e, ens, (C.MutInd _ as t),s) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + | (k, e, ens, (C.MutConstruct _ as t),s) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) -> + let decofix = + function + C.CoFix (i,fl) as t -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + (* the term is the result of a reduction; *) + (* so it is already unwinded. *) + reduce (0,[],[],body',[]) + | C.Appl (C.CoFix (i,fl) :: tl) -> + let (_,_,body) = List.nth fl i in + let body' = + let counter = ref (List.length fl) in + List.fold_right + (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) + fl + body + in + (* the term is the result of a reduction; *) + (* so it is already unwinded. *) + reduce (0,[],[],body',tl) + | t -> t + in + (match decofix (reduce (k,e,ens,term,[])) with + C.MutConstruct (_,_,j,_) -> + reduce (k, e, ens, (List.nth pl (j-1)), s) + | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> + let (arity, r) = + match CicEnvironment.get_obj mutind with + C.InductiveDefinition (tl,ingredients,r) -> + let (_,_,arity,_) = List.nth tl i in + (arity,r) + | _ -> raise WrongUriToInductiveDefinition + in + let ts = + let num_to_eat = r in + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (num_to_eat,tl) in - reduce (0,[], body', tl) - | t -> t + (* ts are already unwinded because they are a sublist of tl *) + reduce (k, e, ens, (List.nth pl (j-1)),(ts@s)) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + ) + | (k, e, ens, (C.Fix (i,fl) as t), s) -> + let (_,recindex,_,body) = List.nth fl i in + let recparam = + try + Some (List.nth s recindex) + with + _ -> None in - (match decofix (reduce (k, e,term,[])) with - C.MutConstruct (_,_,_,j) -> reduce (k, e, (List.nth pl (j-1)), s) - | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> - let (arity, r, num_ingredients) = - match CicEnvironment.get_obj mutind with - C.InductiveDefinition (tl,ingredients,r) -> - let (_,_,arity,_) = List.nth tl i - and num_ingredients = + (match recparam with + Some recparam -> + (match reduce (0,[],[],recparam,[]) with + (* match recparam with *) + C.MutConstruct _ + | C.Appl ((C.MutConstruct _)::_) -> + (* OLD + let body' = + let counter = ref (List.length fl) in List.fold_right - (fun (k,l) i -> - if k < cookingsno then i + List.length l else i - ) ingredients 0 + (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) + fl + body + in + reduce (k, e, ens, body', s) *) + (* NEW *) + let leng = List.length fl in + let fl' = + let unwind_fl (name,recindex,typ,body) = + (name,recindex,unwind k e ens typ, + unwind' leng k e ens body) in - (arity,r,num_ingredients) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - let num_to_eat = r + num_ingredients in - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (num_to_eat,tl) - in - reduce (k, e, (List.nth pl (j-1)),(ts@s)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s) - ) - | (k, e, (C.Fix (i,fl) as t), s) -> - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - Some (List.nth s recindex) - with - _ -> None - in - (match recparam with - Some recparam -> - (match reduce (0,[],recparam,[]) with - (* match recparam with *) - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - (* OLD - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - reduce (k, e, body', s) *) - (* NEW *) - let leng = List.length fl in - let fl' = - let unwind_fl (name,recindex,typ,body) = - (name,recindex,unwind' leng k e typ, unwind' leng k e body) in - List.map unwind_fl fl in + List.map unwind_fl fl + in let new_env = - let counter = ref leng in - let rec build_env e = - if !counter = 0 then e else (decr counter; - build_env ((C.Fix (!counter,fl'))::e)) in - build_env e in - reduce (k+leng, new_env, body,s) - | _ -> let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s) + let counter = ref 0 in + let rec build_env e = + if !counter = leng then e + else + (incr counter ; build_env ((C.Fix (!counter -1, fl'))::e)) + in + build_env e + in + reduce (k+leng, new_env, ens, body, s) + | _ -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) ) - | None -> let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s) - ) - | (k, e,(C.CoFix (i,fl) as t),s) -> let t' = unwind k e t in - if s = [] then t' else C.Appl (t'::s);; + | None -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + ) + | (k, e, ens, (C.CoFix (i,fl) as t),s) -> + let t' = unwind k e ens t in + if s = [] then t' else C.Appl (t'::s) + and push_exp_named_subst k e ens = + function + [] -> ens + | (uri,t)::tl -> push_exp_named_subst k e ((uri,unwind k e ens t)::ens) tl + in + reduce +;; -let rec whd = let module C = Cic in - function - C.Rel _ as t -> t - | C.Var _ as t -> reduce (0, [], t, []) - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> whd te - | C.Prod _ as t -> t - | C.Lambda _ as t -> t - | C.LetIn (n,s,t) -> reduce (1, [s], t, []) - | C.Appl [] -> raise (Impossible 1) - | C.Appl (he::tl) -> reduce (0, [], he, tl) - | C.Const _ as t -> reduce (0, [], t, []) - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase _ as t -> reduce (0, [], t, []) - | C.Fix _ as t -> reduce (0, [], t, []) - | C.CoFix _ as t -> reduce (0, [], t, []) - ;; +let rec whd context t = reduce context (0, [], [], t, []);; -(* let whd t = reduce (0, [],t,[]);; - let res = reduce (0, [],t,[]) in - let rescsc = CicReductionNaif.whd t in - if not (CicReductionNaif.are_convertible res rescsc) then +(* DEBUGGING ONLY +let whd context t = + let res = whd context t in + let rescsc = CicReductionNaif.whd context t in + if not (CicReductionNaif.are_convertible context res rescsc) then begin prerr_endline ("PRIMA: " ^ CicPp.ppterm t) ; flush stderr ; @@ -310,74 +473,136 @@ let rec whd = let module C = Cic in flush stderr ; prerr_endline ("CSC: " ^ CicPp.ppterm rescsc) ; flush stderr ; +CicReductionNaif.fdebug := 0 ; +let _ = CicReductionNaif.are_convertible context res rescsc in assert false ; end else - res ;; *) + res +;; +*) (* t1, t2 must be well-typed *) -let are_convertible = - let rec aux t1 t2 = - if t1 = t2 then true - else +let are_convertible = + let module U = UriManager in + let rec aux context t1 t2 = let aux2 t1 t2 = - let module U = UriManager in - let module C = Cic in - match (t1,t2) with - (C.Rel n1, C.Rel n2) -> n1 = n2 - | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 - | (C.Meta n1, C.Meta n2) -> n1 = n2 - | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) - | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) -> - aux s1 s2 && aux t1 t2 - | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) -> - aux s1 s2 && aux t1 t2 - | (C.Appl l1, C.Appl l2) -> - (try - List.fold_right2 (fun x y b -> aux x y && b) l1 l2 true - with - Invalid_argument _ -> false - ) - | (C.Const (uri1,_), C.Const (uri2,_)) -> - U.eq uri1 uri2 - | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> - U.eq uri1 uri2 && i1 = i2 - | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> - U.eq uri1 uri2 && i1 = i2 && j1 = j2 - | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), - C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> - (* aux outtype1 outtype2 should be true if aux pl1 pl2 *) - U.eq uri1 uri2 && i1 = i2 && aux outtype1 outtype2 && - aux term1 term2 && - List.fold_right2 (fun x y b -> b && aux x y) pl1 pl2 true - | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - i1 = i2 && - List.fold_right2 - (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> - b && recindex1 = recindex2 && aux ty1 ty2 && aux bo1 bo2) - fl1 fl2 true - | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - i1 = i2 && - List.fold_right2 - (fun (_,ty1,bo1) (_,ty2,bo2) b -> - b && aux ty1 ty2 && aux bo1 bo2) - fl1 fl2 true - | (_,_) -> false + (* this trivial euristic cuts down the total time of about five times ;-) *) + (* this because most of the time t1 and t2 are "sintactically" the same *) + if t1 = t2 then + true + else + begin + let module C = Cic in + match (t1,t2) with + (C.Rel n1, C.Rel n2) -> n1 = n2 + | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) -> + U.eq uri1 uri2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.Meta (n1,l1), C.Meta (n2,l2)) -> + n1 = n2 && + List.fold_left2 + (fun b t1 t2 -> + b && + match t1,t2 with + None,_ + | _,None -> true + | Some t1',Some t2' -> aux context t1' t2' + ) true l1 l2 + | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> + aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 + | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2 + | (C.Appl l1, C.Appl l2) -> + (try + List.fold_right2 (fun x y b -> aux context x y && b) l1 l2 true + with + Invalid_argument _ -> false + ) + | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> + U.eq uri1 uri2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutInd (uri1,i1,exp_named_subst1), + C.MutInd (uri2,i2,exp_named_subst2) + ) -> + U.eq uri1 uri2 && i1 = i2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), + C.MutConstruct (uri2,i2,j2,exp_named_subst2) + ) -> + U.eq uri1 uri2 && i1 = i2 && j1 = j2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutCase (uri1,i1,outtype1,term1,pl1), + C.MutCase (uri2,i2,outtype2,term2,pl2)) -> + U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 && + aux context term1 term2 && + List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true + | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> + let tys = + List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 + in + i1 = i2 && + List.fold_right2 + (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) b -> + b && recindex1 = recindex2 && aux context ty1 ty2 && + aux (tys@context) bo1 bo2) + fl1 fl2 true + | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> + let tys = + List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 + in + i1 = i2 && + List.fold_right2 + (fun (_,ty1,bo1) (_,ty2,bo2) b -> + b && aux context ty1 ty2 && aux (tys@context) bo1 bo2) + fl1 fl2 true + | (C.Cast _, _) | (_, C.Cast _) + | (C.Implicit, _) | (_, C.Implicit) -> + raise (Impossible 3) (* we don't trust our whd ;-) *) + | (_,_) -> false + end in if aux2 t1 t2 then true - else aux2 (whd t1) (whd t2) -in - aux -;; - - - - - - - - - - - + else + begin + debug t1 [t2] "PREWHD"; + let t1' = whd context t1 + and t2' = whd context t2 in + debug t1' [t2'] "POSTWHD"; + aux2 t1' t2' + end + in + aux +;; diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli index d61bc7251..7a6255003 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.mli +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.mli @@ -24,11 +24,10 @@ *) exception WrongUriToInductiveDefinition -exception ReferenceToDefinition -exception ReferenceToAxiom +exception ReferenceToConstant exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition val fdebug : int ref -val whd : Cic.term -> Cic.term -val are_convertible : Cic.term -> Cic.term -> bool +val whd : Cic.context -> Cic.term -> Cic.term +val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index f569e75cd..f7ddd1968 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -31,18 +31,14 @@ 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, t)) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i in if !fdebug = 0 then - begin - print_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ; - flush stdout - end + prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "") ;; exception Impossible of int;; -exception ReferenceToDefinition;; -exception ReferenceToAxiom;; +exception ReferenceToConstant;; exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; @@ -60,14 +56,14 @@ let whd context = | Some (_, C.Def bo) -> whdaux l (S.lift n bo) | None -> raise RelToHiddenHypothesis ) - | C.Var uri as t -> - (match CicEnvironment.get_cooked_obj uri 0 with - C.Definition _ -> raise ReferenceToDefinition - | C.Axiom _ -> raise ReferenceToAxiom + | C.Var (uri,exp_named_subst) as t -> + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant | 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.Variable (_,None,_,_) -> if l = [] then t else C.Appl (t::l) + | C.Variable (_,Some body,_,_) -> + whdaux l (CicSubstitution.subst_vars exp_named_subst body) ) | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) | C.Sort _ as t -> t (* l should be empty *) @@ -83,17 +79,19 @@ let whd context = | C.LetIn (n,s,t) -> whdaux l (S.subst (whdaux [] s) t) | C.Appl (he::tl) -> whdaux (tl@l) he | C.Appl [] -> raise (Impossible 1) - | C.Const (uri,cookingsno) as t -> - (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) + | C.Const (uri,exp_named_subst) as t -> + (match CicEnvironment.get_cooked_obj uri with + C.Constant (_,Some body,_,_) -> + whdaux l (CicSubstitution.subst_vars exp_named_subst body) + | C.Constant _ -> if l = [] then t else C.Appl (t::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_) -> whdaux l body + | C.CurrentProof (_,_,body,_,_) -> + whdaux l (CicSubstitution.subst_vars exp_named_subst body) | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) - | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l) - | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l) - | C.MutCase (mutind,cookingsno,i,_,term,pl) as t-> + | C.MutInd _ as t -> if l = [] then t else C.Appl (t::l) + | C.MutConstruct _ as t -> if l = [] then t else C.Appl (t::l) + | C.MutCase (mutind,i,_,term,pl) as t-> let decofix = function C.CoFix (i,fl) as t -> @@ -119,35 +117,28 @@ let whd context = | t -> t in (match decofix (whdaux [] term) with - C.MutConstruct (_,_,_,j) -> whdaux l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,_,j) :: tl) -> - let (arity, r, num_ingredients) = + C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1)) + | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> + let (arity, r) = match CicEnvironment.get_obj mutind with C.InductiveDefinition (tl,ingredients,r) -> - let (_,_,arity,_) = List.nth tl i - and num_ingredients = - List.fold_right - (fun (k,l) i -> - if k < cookingsno then i + List.length l else i - ) ingredients 0 - in - (arity,r,num_ingredients) + let (_,_,arity,_) = List.nth tl i in + (arity,r) | _ -> raise WrongUriToInductiveDefinition in let ts = - let num_to_eat = r + num_ingredients in - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (num_to_eat,tl) + let rec eat_first = + function + (0,l) -> l + | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) + | _ -> raise (Impossible 5) + in + eat_first (r,tl) in whdaux (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> if l = [] then t else C.Appl (t::l) + | C.Cast _ | C.Implicit -> + raise (Impossible 2) (* we don't trust our whd ;-) *) + | _ -> if l = [] then t else C.Appl (t::l) ) | C.Fix (i,fl) as t -> let (_,recindex,_,body) = List.nth fl i in @@ -204,7 +195,16 @@ let are_convertible = let module C = Cic in match (t1,t2) with (C.Rel n1, C.Rel n2) -> n1 = n2 - | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2 + | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) -> + U.eq uri1 uri2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) | (C.Meta (n1,l1), C.Meta (n2,l2)) -> n1 = n2 && List.fold_left2 @@ -228,31 +228,42 @@ let are_convertible = with Invalid_argument _ -> false ) - | (C.Const (uri1,_), C.Const (uri2,_)) -> - (*CSC: questo commento e' chiaro o delirante? Io lo sto scrivendo *) - (*CSC: mentre sono delirante, quindi ... *) - (* WARNING: it is really important that the two cookingsno are not*) - (* checked for equality. This allows not to cook an object with no*) - (* ingredients only to update the cookingsno. E.g: if a term t has*) - (* a reference to a term t1 which does not depend on any variable *) - (* and t1 depends on a term t2 (that can't depend on any variable *) - (* because of t1), then t1 cooked at every level could be the same*) - (* as t1 cooked at level 0. Doing so, t2 will be extended in t *) - (* with cookingsno 0 and not 2. But this will not cause any *) - (* trouble if here we don't check that the two cookingsno are *) - (* equal. *) - U.eq uri1 uri2 - | (C.MutInd (uri1,k1,i1), C.MutInd (uri2,k2,i2)) -> - (* WARNIG: see the previous warning *) - U.eq uri1 uri2 && i1 = i2 - | (C.MutConstruct (uri1,_,i1,j1), C.MutConstruct (uri2,_,i2,j2)) -> - (* WARNIG: see the previous warning *) - U.eq uri1 uri2 && i1 = i2 && j1 = j2 - | (C.MutCase (uri1,_,i1,outtype1,term1,pl1), - C.MutCase (uri2,_,i2,outtype2,term2,pl2)) -> - (* WARNIG: see the previous warning *) - (* aux context outtype1 outtype2 should be true if *) - (* aux context pl1 pl2 *) + | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) -> + U.eq uri1 uri2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutInd (uri1,i1,exp_named_subst1), + C.MutInd (uri2,i2,exp_named_subst2) + ) -> + U.eq uri1 uri2 && i1 = i2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutConstruct (uri1,i1,j1,exp_named_subst1), + C.MutConstruct (uri2,i2,j2,exp_named_subst2) + ) -> + U.eq uri1 uri2 && i1 = i2 && j1 = j2 && + (try + List.fold_right2 + (fun (uri1,x) (uri2,y) b -> + U.eq uri1 uri2 && aux context x y && b + ) exp_named_subst1 exp_named_subst2 true + with + Invalid_argument _ -> false + ) + | (C.MutCase (uri1,i1,outtype1,term1,pl1), + C.MutCase (uri2,i2,outtype2,term2,pl2)) -> U.eq uri1 uri2 && i1 = i2 && aux context outtype1 outtype2 && aux context term1 term2 && List.fold_right2 (fun x y b -> b && aux context x y) pl1 pl2 true diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli index d61bc7251..7a6255003 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.mli +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.mli @@ -24,11 +24,10 @@ *) exception WrongUriToInductiveDefinition -exception ReferenceToDefinition -exception ReferenceToAxiom +exception ReferenceToConstant exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition val fdebug : int ref -val whd : Cic.term -> Cic.term -val are_convertible : Cic.term -> Cic.term -> bool +val whd : Cic.context -> Cic.term -> Cic.term +val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index f312f556c..002ea28df 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -25,6 +25,10 @@ exception CannotSubstInMeta;; exception RelToHiddenHypothesis;; +exception ReferenceToVariable;; +exception ReferenceToConstant;; +exception ReferenceToCurrentProof;; +exception ReferenceToInductiveDefinition;; let lift n = let rec liftaux k = @@ -35,7 +39,11 @@ let lift n = C.Rel m else C.Rel (m + n) - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') | C.Meta (i,l) -> let l' = List.map @@ -52,11 +60,23 @@ let lift n = | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) | C.Appl l -> C.Appl (List.map (liftaux k) l) - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, liftaux k outty, liftaux k t, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, liftaux k outty, liftaux k t, List.map (liftaux k) pl) | C.Fix (i, fl) -> let len = List.length fl in @@ -91,7 +111,11 @@ let subst arg = | n when n < k -> t | _ -> C.Rel (n - 1) ) - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') | C.Meta (i, l) as t -> let l' = List.map @@ -116,11 +140,23 @@ let subst arg = | _ as he' -> C.Appl (he'::tl') end | C.Appl _ -> assert false - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k outt, substaux k t, List.map (substaux k) pl) | C.Fix (i,fl) -> let len = List.length fl in @@ -142,35 +178,164 @@ let subst arg = substaux 1 ;; -let undebrujin_inductive_def uri = - function - Cic.InductiveDefinition (dl,params,n_ind_params) -> - let dl' = - List.map - (fun (name,inductive,arity,constructors) -> - let constructors' = - List.map - (fun (name,ty,r) -> - let ty' = - let counter = ref (List.length dl) in - List.fold_right - (fun _ -> - decr counter ; - subst (Cic.MutInd (uri,0,!counter)) - ) dl ty - in - (name,ty',r) - ) constructors +(*CSC: i controlli di tipo debbono essere svolti da destra a *) +(*CSC: sinistra: i{B/A;b/a} ==> a{B/A;b/a} ==> a{b/a{B/A}} ==> b *) +(*CSC: la sostituzione ora e' implementata in maniera simultanea, ma *) +(*CSC: dovrebbe diventare da sinistra verso destra: *) +(*CSC: t{a=a/A;b/a} ==> \H:a=a.H{b/a} ==> \H:b=b.H *) +(*CSC: per la roba che proviene da Coq questo non serve! *) +let subst_vars exp_named_subst = +(* +prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; +*) + let rec substaux k = + let module C = Cic in + function + C.Rel _ as t -> t + | C.Var (uri,exp_named_subst') -> + (try + let (_,arg) = + List.find + (function (varuri,_) -> UriManager.eq uri varuri) exp_named_subst in - (name,inductive,arity,constructors') - ) dl - in - Cic.InductiveDefinition (dl', params, n_ind_params) - | obj -> obj + lift (k -1) arg + with + Not_found -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable (_,_,_,params) -> params + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in +(* +prerr_endline "\n\n---- BEGIN " ; +prerr_endline ("----params: " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ; +prerr_endline ("----S(" ^ UriManager.string_of_uri uri ^ "): " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst)) ; +prerr_endline ("----P: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst')) ; +*) + let exp_named_subst'' = + substaux_in_exp_named_subst uri k exp_named_subst' params + in +(* +prerr_endline ("----D: " ^ String.concat " ; " (List.map (function (uri,_) -> UriManager.string_of_uri uri) exp_named_subst'')) ; +prerr_endline "---- END\n\n " ; +*) + C.Var (uri,exp_named_subst'') + ) + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const (uri,exp_named_subst') -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant (_,_,_,params) -> params + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof (_,_,_,_,params) -> params + | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + ) + in + let exp_named_subst'' = + substaux_in_exp_named_subst uri k exp_named_subst' params + in + C.Const (uri,exp_named_subst'') + | C.MutInd (uri,typeno,exp_named_subst') -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition (_,params,_) -> params + ) + in + let exp_named_subst'' = + substaux_in_exp_named_subst uri k exp_named_subst' params + in + C.MutInd (uri,typeno,exp_named_subst'') + | C.MutConstruct (uri,typeno,consno,exp_named_subst') -> + let params = + (match CicEnvironment.get_cooked_obj uri with + C.Constant _ -> raise ReferenceToConstant + | C.Variable _ -> raise ReferenceToVariable + | C.CurrentProof _ -> raise ReferenceToCurrentProof + | C.InductiveDefinition (_,params,_) -> params + ) + in + let exp_named_subst'' = + substaux_in_exp_named_subst uri k exp_named_subst' params + in + C.MutConstruct (uri,typeno,consno,exp_named_subst'') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + and substaux_in_exp_named_subst uri k exp_named_subst' params = +(*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) +(*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) + let rec filter_and_lift = + function + [] -> [] + | (uri,t)::tl when + List.for_all + (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' + && + List.mem uri params + -> + (uri,lift (k-1) t)::(filter_and_lift tl) + | _::tl -> filter_and_lift tl +(* + | (uri,_)::tl -> +prerr_endline ("---- SKIPPO " ^ UriManager.string_of_uri uri) ; +if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) exp_named_subst' then prerr_endline "---- OK1" ; +prerr_endline ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ; +if List.mem uri params then prerr_endline "---- OK2" ; + filter_and_lift tl +*) + in + List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst' @ + (filter_and_lift exp_named_subst) + in + substaux 1 ;; (* l is the relocation list *) - let lift_meta l t = let module C = Cic in if l = [] then t else @@ -184,7 +349,11 @@ let lift_meta l t = with (Failure _) -> assert false ) - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') | C.Meta (i,l) -> let l' = List.map @@ -205,12 +374,23 @@ let lift_meta l 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 l -> C.Appl (List.map (aux k) l) - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,aux k outt, aux k t, - List.map (aux k) pl) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,aux k outt, aux k t, List.map (aux k) pl) | C.Fix (i,fl) -> let len = List.length fl in let substitutedfl = diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 8915b814a..038b5de3f 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -23,7 +23,24 @@ * http://cs.unibo.it/helm/. *) +exception CannotSubstInMeta;; +exception RelToHiddenHypothesis;; +exception ReferenceToVariable;; +exception ReferenceToConstant;; +exception ReferenceToInductiveDefinition;; + +(* lift n t *) +(* lifts [t] of [n] *) val lift : int -> Cic.term -> Cic.term + +(* subst t1 t2 *) +(* substitutes [t1] for [Rel 1] in [t2] *) val subst : Cic.term -> Cic.term -> Cic.term + +(* subst_vars exp_named_subst t2 *) +(* applies [exp_named_subst] to [t2] *) +val subst_vars : + Cic.term Cic.explicit_named_substitution -> Cic.term -> Cic.term + +(* ?????????? *) val lift_meta : (Cic.term option) list -> Cic.term -> Cic.term -val undebrujin_inductive_def : UriManager.uri -> Cic.obj -> Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 11d68b78c..ce5275470 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -40,7 +40,7 @@ let debug t context = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, 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::context) "")) @@ -54,27 +54,90 @@ let rec split l n = | (_,_) -> raise ListTooShort ;; +let debrujin_constructor uri number_of_types = + let rec aux k = + let module C = Cic in + function + C.Rel _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta _ -> assert false + | C.Sort _ + | C.Implicit as t -> t + | 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 l -> C.Appl (List.map (aux k) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> + if exp_named_subst != [] then + raise + (NotWellTyped + ("Debrujin: a non-empty explicit named substitution is applied to " ^ + "a mutual inductive type which is being defined")) ; + C.Rel (k + number_of_types - tyno) ; + | C.MutInd (uri',tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutInd (uri',tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, aux k outty, aux k t, + List.map (aux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + aux 0 +;; + exception CicEnvironmentError;; -let rec cooked_type_of_constant uri cookingsno = +let rec type_of_constant uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri cookingsno with + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; (* let's typecheck the uncooked obj *) (match uobj with - C.Definition (_,te,ty,_) -> + C.Constant (_,Some te,ty,_) -> let _ = type_of ty in if not (R.are_convertible [] (type_of te) ty) then raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) - | C.Axiom (_,ty,_) -> + | C.Constant (_,None,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in () - | C.CurrentProof (_,conjs,te,ty) -> + | C.CurrentProof (_,conjs,te,ty,_) -> (*CSC: bisogna controllare anche il metasenv!!! *) let _ = type_of_aux' conjs [] ty in if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) @@ -84,14 +147,13 @@ let rec cooked_type_of_constant uri cookingsno = ) ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - match CicEnvironment.is_type_checked uri cookingsno with + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError in match cobj with - C.Definition (_,_,ty,_) -> ty - | C.Axiom (_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty) -> ty + C.Constant (_,_,ty,_) -> ty + | C.CurrentProof (_,_,_,ty,_) -> ty | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) and type_of_variable uri = @@ -99,9 +161,9 @@ and type_of_variable uri = let module R = CicReduction in let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) - match CicEnvironment.is_type_checked uri 0 with - CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty - | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) -> + match CicEnvironment.is_type_checked uri with + CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty + | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> Logger.log (`Start_type_checking uri) ; (* only to check that ty is well-typed *) let _ = type_of ty in @@ -124,7 +186,6 @@ and does_not_occur context n nn te = match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> false | C.Rel _ - | C.Var _ | C.Meta _ | C.Sort _ | C.Implicit -> true @@ -141,10 +202,13 @@ and does_not_occur context n nn te = does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur context n nn x) l true - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ -> true - | C.MutCase (_,_,_,out,te,pl) -> + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x) + exp_named_subst true + | C.MutCase (_,_,out,te,pl) -> does_not_occur context n nn out && does_not_occur context n nn te && List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true | C.Fix (_,fl) -> @@ -181,14 +245,14 @@ and weakly_positive context n nn uri te = let module C = Cic in (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) let dummy_mutind = - C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,0) + C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[]) in (*CSC mettere in cicSubstitution *) let rec subst_inductive_type_with_dummy_mutind = function - C.MutInd (uri',_,0) when UriManager.eq uri' uri -> + C.MutInd (uri',0,_) when UriManager.eq uri' uri -> dummy_mutind - | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> + | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> dummy_mutind | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te | C.Prod (name,so,ta) -> @@ -199,8 +263,8 @@ and weakly_positive context n nn uri te = subst_inductive_type_with_dummy_mutind ta) | C.Appl tl -> C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) - | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> - C.MutCase (uri,cookingsno,i, + | C.MutCase (uri,i,outtype,term,pl) -> + C.MutCase (uri,i, subst_inductive_type_with_dummy_mutind outtype, subst_inductive_type_with_dummy_mutind term, List.map subst_inductive_type_with_dummy_mutind pl) @@ -212,15 +276,36 @@ and weakly_positive context n nn uri te = C.CoFix (i,List.map (fun (name,ty,bo) -> (name, subst_inductive_type_with_dummy_mutind ty, subst_inductive_type_with_dummy_mutind bo)) fl) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') | t -> t in match CicReduction.whd context te with - C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true - | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true - | C.Prod (C.Anonimous,source,dest) -> + C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true + | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true + | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (C.Anonimous,(C.Decl source)))::context) + weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) when does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> @@ -261,7 +346,7 @@ and strictly_positive context n nn te = strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - | C.Appl ((C.MutInd (uri,_,i))::tl) -> + | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> let (ok,paramsno,ity,cl,name) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> @@ -272,7 +357,11 @@ and strictly_positive context n nn te = let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in let cl' = - List.map (fun (_,te,_) -> instantiate_parameters lifted_params te) cl + List.map + (fun (_,te) -> + instantiate_parameters lifted_params + (CicSubstitution.subst_vars exp_named_subst te) + ) cl in ok && List.fold_right @@ -314,10 +403,10 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = true else raise (WrongRequiredArgument (UriManager.string_of_uri uri)) - | C.Prod (C.Anonimous,source,dest) -> + | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn source && are_all_occurrences_positive - ((Some (C.Anonimous,(C.Decl source)))::context) uri indparamsno + ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) when does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> @@ -332,8 +421,9 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)) -(*CSC: cambiare il nome, torna unit! *) -and cooked_mutual_inductive_defs uri = +(* Main function to checks the correctness of a mutual *) +(* inductive block definition. *) +and check_mutual_inductive_defs uri = let module U = UriManager in function Cic.InductiveDefinition (itl, _, indparamsno) -> @@ -346,34 +436,28 @@ and cooked_mutual_inductive_defs uri = (* In order not to use type_of_aux we put the types of the *) (* mutual inductive types at the head of the types of the *) (* constructors using Prods *) - (*CSC: piccola??? inefficienza *) let len = List.length itl in -(*CSC: siamo sicuri che non debba fare anche un List.rev? Il bug *) -(*CSC: si manifesterebbe solamene con tipi veramente mutualmente *) -(*CSC: induttivi... *) let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in let _ = List.fold_right (fun (_,_,_,cl) i -> List.iter - (fun (name,te,r) -> + (fun (name,te) -> + let debrujinedte = debrujin_constructor uri len te in let augmented_term = List.fold_right (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl te + itl debrujinedte in let _ = type_of augmented_term in (* let's check also the positivity conditions *) if not - (are_all_occurrences_positive tys uri indparamsno i 0 len te) + (are_all_occurrences_positive tys uri indparamsno i 0 len + debrujinedte) then raise (NotPositiveOccurrences (U.string_of_uri uri)) - else - match !r with - Some _ -> raise (Impossible 2) - | None -> r := Some (recursive_args tys 0 len te) ) cl ; (i + 1) ) itl 1 @@ -382,19 +466,19 @@ and cooked_mutual_inductive_defs uri = | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -and cooked_type_of_mutual_inductive_defs uri cookingsno i = +and type_of_mutual_inductive_defs uri i = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri cookingsno with + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; - cooked_mutual_inductive_defs uri uobj ; + check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked uri cookingsno with + (match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) @@ -405,19 +489,19 @@ and cooked_type_of_mutual_inductive_defs uri cookingsno i = arity | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) -and cooked_type_of_mutual_inductive_constr uri cookingsno i j = +and type_of_mutual_inductive_constr uri i j = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri cookingsno with + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; - cooked_mutual_inductive_defs uri uobj ; + check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked uri cookingsno with + (match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) @@ -425,7 +509,7 @@ and cooked_type_of_mutual_inductive_constr uri cookingsno i j = match cobj with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cl) = List.nth dl i in - let (_,ty,_) = List.nth cl (j-1) in + let (_,ty) = List.nth cl (j-1) in ty | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -538,10 +622,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = | C.Const _ | C.MutInd _ -> raise (Impossible 12) | C.MutConstruct _ -> false - | C.MutCase (uri,_,i,outtype,term,pl) -> + | C.MutCase (uri,i,outtype,term,pl) -> (match term with C.Rel m when List.mem m safes || m = x -> - let (isinductive,paramsno,cl) = + let (tys,len,isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let tys = @@ -550,10 +634,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = let (_,isinductive,_,cl) = List.nth tl i in let cl' = List.map - (fun (id,ty,r) -> - (id, snd (split_prods tys paramsno ty), r)) cl + (fun (id,ty) -> + (id, ty, snd (split_prods tys paramsno ty))) cl in - (isinductive,paramsno,cl') + (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in @@ -564,13 +648,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = pl true else List.fold_right - (fun (p,(_,c,rl)) i -> + (fun (p,(_,te,c)) i -> let rl' = - match !rl with - Some rl' -> - let (_,rl'') = split rl' paramsno in - rl'' - | None -> raise (Impossible 13) + let debrujinedte = debrujin_constructor uri len te in + recursive_args tys 0 len debrujinedte in let (e,safes',n',nn',x',context') = get_new_safes context p c rl' safes n nn x @@ -579,7 +660,7 @@ and check_is_really_smaller_arg context n nn kl x safes te = check_is_really_smaller_arg context' n' nn' kl x' safes' e ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (isinductive,paramsno,cl) = + let (tys,len,isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -588,10 +669,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = in let cl' = List.map - (fun (id,ty,r) -> - (id, snd (split_prods tys paramsno ty), r)) cl + (fun (id,ty) -> + (id, ty, snd (split_prods tys paramsno ty))) cl in - (isinductive,paramsno,cl') + (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in @@ -604,13 +685,10 @@ and check_is_really_smaller_arg context n nn kl x safes te = (*CSC: supponiamo come prima che nessun controllo sia necessario*) (*CSC: sugli argomenti di una applicazione *) List.fold_right - (fun (p,(_,c,rl)) i -> + (fun (p,(_,te,c)) i -> let rl' = - match !rl with - Some rl' -> - let (_,rl'') = split rl' paramsno in - rl'' - | None -> raise (Impossible 14) + let debrujinedte = debrujin_constructor uri len te in + recursive_args tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes context p c rl' safes n nn x @@ -662,7 +740,6 @@ and guarded_by_destructors context n nn kl x safes = | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo | None -> raise RelToHiddenHypothesis ) - | C.Var _ | C.Meta _ | C.Sort _ | C.Implicit -> true @@ -694,13 +771,17 @@ and guarded_by_destructors context n nn kl x safes = List.fold_right (fun t i -> i && guarded_by_destructors context n nn kl x safes t) tl true - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ -> true - | C.MutCase (uri,_,i,outtype,term,pl) -> + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) + | C.MutInd (_,_,exp_named_subst) + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_right + (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t) + exp_named_subst true + | C.MutCase (uri,i,outtype,term,pl) -> (match term with C.Rel m when List.mem m safes || m = x -> - let (isinductive,paramsno,cl) = + let (tys,len,isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -709,10 +790,10 @@ and guarded_by_destructors context n nn kl x safes = in let cl' = List.map - (fun (id,ty,r) -> - (id, snd (split_prods tys paramsno ty), r)) cl + (fun (id,ty) -> + (id, ty, snd (split_prods tys paramsno ty))) cl in - (isinductive,paramsno,cl') + (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in @@ -728,13 +809,10 @@ and guarded_by_destructors context n nn kl x safes = guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun (p,(_,c,rl)) i -> + (fun (p,(_,te,c)) i -> let rl' = - match !rl with - Some rl' -> - let (_,rl'') = split rl' paramsno in - rl'' - | None -> raise (Impossible 15) + let debrujinedte = debrujin_constructor uri len te in + recursive_args tys 0 len debrujinedte in let (e,safes',n',nn',x',context') = get_new_safes context p c rl' safes n nn x @@ -743,7 +821,7 @@ and guarded_by_destructors context n nn kl x safes = guarded_by_destructors context' n' nn' kl x' safes' e ) (List.combine pl cl) true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (isinductive,paramsno,cl) = + let (tys,len,isinductive,paramsno,cl) = match CicEnvironment.get_obj uri with C.InductiveDefinition (tl,_,paramsno) -> let (_,isinductive,_,cl) = List.nth tl i in @@ -752,10 +830,10 @@ and guarded_by_destructors context n nn kl x safes = in let cl' = List.map - (fun (id,ty,r) -> - (id, snd (split_prods tys paramsno ty), r)) cl + (fun (id,ty) -> + (id, ty, snd (split_prods tys paramsno ty))) cl in - (isinductive,paramsno,cl') + (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) in @@ -775,13 +853,10 @@ and guarded_by_destructors context n nn kl x safes = i && guarded_by_destructors context n nn kl x safes t) tl true && List.fold_right - (fun (p,(_,c,rl)) i -> + (fun (p,(_,te,c)) i -> let rl' = - match !rl with - Some rl' -> - let (_,rl'') = split rl' paramsno in - rl'' - | None -> raise (Impossible 16) + let debrujinedte = debrujin_constructor uri len te in + recursive_args tys 0 len debrujinedte in let (e, safes',n',nn',x',context') = get_new_safes context p c rl' safes n nn x @@ -836,8 +911,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) match CicReduction.whd context te with C.Rel m when m > n && m <= nn -> h - | C.Rel _ - | C.Var _ -> true + | C.Rel _ -> true | C.Meta _ | C.Sort _ | C.Implicit @@ -852,12 +926,13 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> h && List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) -> + | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> let consty = - match CicEnvironment.get_cooked_obj uri cookingsno with + match CicEnvironment.get_cooked_obj uri with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in - let (_,cons,_) = List.nth cl (j - 1) in cons + let (_,cons) = List.nth cl (j - 1) in + CicSubstitution.subst_vars exp_named_subst cons | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) @@ -875,10 +950,10 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = analyse_branch ((Some (name,(C.Decl so)))::context) de te | C.Lambda _ | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *) - | C.Appl ((C.MutInd (uri,_,_))::tl) as ty + | C.Appl ((C.MutInd (uri,_,_))::_) as ty when uri == coInductiveTypeURI -> guarded_by_constructors context n nn true te [] coInductiveTypeURI - | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> + | C.Appl ((C.MutInd (uri,_,_))::_) as ty -> guarded_by_constructors context n nn true te tl coInductiveTypeURI | C.Appl _ -> does_not_occur context n nn te @@ -963,7 +1038,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo args coInductiveTypeURI ) fl true - | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) -> + | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) -> List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl && does_not_occur context n nn out && does_not_occur context n nn te && @@ -974,10 +1049,15 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = ) pl true | C.Appl l -> List.fold_right (fun x i -> i && does_not_occur context n nn x) l true - | C.Const _ -> true + | C.Var (_,exp_named_subst) + | C.Const (_,exp_named_subst) -> + List.fold_right + (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true | C.MutInd _ -> assert false - | C.MutConstruct _ -> true - | C.MutCase (_,_,_,out,te,pl) -> + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.fold_right + (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true + | C.MutCase (_,_,out,te,pl) -> does_not_occur context n nn out && does_not_occur context n nn te && List.fold_right @@ -1018,12 +1098,14 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = check_allowed_sort_elimination context uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true - | (C.Sort C.Prop, C.Sort C.Set) when need_dummy -> + | (C.Sort C.Prop, C.Sort C.Set) + | (C.Sort C.Prop, C.Sort C.Type) when need_dummy -> +(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in - (* is a singleton definition? *) - List.length cl = 1 + (* is a singleton definition or the empty proposition? *) + List.length cl = 1 || List.length cl = 0 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ) @@ -1037,7 +1119,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = in let (_,_,_,cl) = List.nth itl i in List.fold_right - (fun (_,x,_) i -> i && is_small tys paramsno x) cl true + (fun (_,x) i -> i && is_small tys paramsno x) cl true | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ) @@ -1076,7 +1158,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in List.fold_right - (fun (_,x,_) i -> i && is_small tys paramsno x) cl true + (fun (_,x) i -> i && is_small tys paramsno x) cl true | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -1109,7 +1191,7 @@ and type_of_branch context argsno need_dummy outtype term constype = C.Appl l -> C.Appl (l@[C.Rel 1]) | t -> C.Appl [t ; C.Rel 1] in - C.Prod (C.Anonimous,so,type_of_branch + C.Prod (C.Anonymous,so,type_of_branch ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) | _ -> raise (Impossible 20) @@ -1165,9 +1247,12 @@ and type_of_aux' metasenv context t = with _ -> raise (NotWellTyped "Not a close term") ) - | C.Var uri -> + | C.Var (uri,exp_named_subst) -> incr fdebug ; - let ty = type_of_variable uri in + check_exp_named_subst context exp_named_subst ; + let ty = + CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) + in decr fdebug ; ty | C.Meta (n,l) -> @@ -1196,27 +1281,50 @@ and type_of_aux' metasenv context t = | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) let _ = type_of_aux context s in - C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t) + (* The type of a LetIn is a LetIn. Extremely slow since the computed + LetIn is later reduced and maybe also re-checked. + (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)) + *) + (* The type of the LetIn is reduced. Much faster than the previous + solution. Moreover the inferred type is probably very different + from the expected one. + (CicReduction.whd context + (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))) + *) + (* One-step LetIn reduction. Even faster than the previous solution. + Moreover the inferred type is closer to the expected one. *) + (CicSubstitution.subst s + (type_of_aux ((Some (n,(C.Def s)))::context) t)) | C.Appl (he::tl) when List.length tl > 0 -> let hetype = type_of_aux context he and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in eat_prods context hetype tlbody_and_type | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") - | C.Const (uri,cookingsno) -> + | C.Const (uri,exp_named_subst) -> incr fdebug ; - let cty = cooked_type_of_constant uri cookingsno in + check_exp_named_subst context exp_named_subst ; + let cty = + CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + in decr fdebug ; cty - | C.MutInd (uri,cookingsno,i) -> + | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; - let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in + check_exp_named_subst context exp_named_subst ; + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_defs uri i) + in decr fdebug ; cty - | C.MutConstruct (uri,cookingsno,i,j) -> - let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j + | C.MutConstruct (uri,i,j,exp_named_subst) -> + check_exp_named_subst context exp_named_subst ; + let cty = + CicSubstitution.subst_vars exp_named_subst + (type_of_mutual_inductive_constr uri i j) in cty - | C.MutCase (uri,cookingsno,i,outtype,term,pl) -> + | C.MutCase (uri,i,outtype,term,pl) -> let outsort = type_of_aux context outtype in let (need_dummy, k) = let rec guess_args context t = @@ -1227,9 +1335,11 @@ and type_of_aux' metasenv context t = if n = 0 then (* last prod before sort *) match CicReduction.whd context s with - (*CSC vedi nota delirante su cookingsno in cicReduction.ml *) - C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1) - | C.Appl ((C.MutInd (uri',_,i')) :: _) +(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) +(*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) + | C.Appl ((C.MutInd (uri',i',_)) :: _) when U.eq uri' uri && i' = i -> (false, 1) | _ -> (true, 1) else @@ -1240,30 +1350,35 @@ and type_of_aux' metasenv context t = let (b, k) = guess_args context outsort in if not b then (b, k - 1) else (b, k) in - let (parameters, arguments) = + let (parameters, arguments, exp_named_subst) = match R.whd context (type_of_aux context term) with (*CSC manca il caso dei CAST *) - C.MutInd (uri',_,i') -> - (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*) - if U.eq uri uri' && i = i' then ([],[]) +(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) +(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) +(*CSC: Hint: nella DTD servono per gli stylesheet. *) + C.MutInd (uri',i',exp_named_subst) as typ -> + if U.eq uri uri' && i = i' then ([],[],exp_named_subst) else raise (NotWellTyped ("MutCase: the term is of type " ^ - (U.string_of_uri uri') ^ "," ^ string_of_int i' ^ - " instead of type " ^ (U.string_of_uri uri') ^ "," ^ - string_of_int i)) - | C.Appl (C.MutInd (uri',_,i') :: tl) -> - if U.eq uri uri' && i = i' then split tl (List.length tl - k) + CicPp.ppterm typ ^ + " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^ + string_of_int i ^ "{_}")) + | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) -> + if U.eq uri uri' && i = i' then + let params,args = + split tl (List.length tl - k) + in params,args,exp_named_subst else raise (NotWellTyped ("MutCase: the term is of type " ^ - (U.string_of_uri uri') ^ "," ^ string_of_int i' ^ - " instead of type " ^ (U.string_of_uri uri) ^ "," ^ - string_of_int i)) + CicPp.ppterm typ ^ + " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^ + string_of_int i ^ "{_}")) | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one") in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let sort_of_ind_type = if parameters = [] then - C.MutInd (uri,cookingsno,i) + C.MutInd (uri,i,exp_named_subst) else - C.Appl ((C.MutInd (uri,cookingsno,i))::parameters) + C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in if not (check_allowed_sort_elimination context uri i need_dummy sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) @@ -1271,28 +1386,32 @@ and type_of_aux' metasenv context t = raise (NotWellTyped "MutCase: not allowed sort elimination") ; (* let's check if the type of branches are right *) - let (cl,parsno) = - match CicEnvironment.get_cooked_obj uri cookingsno with - C.InductiveDefinition (tl,_,parsno) -> - let (_,_,_,cl) = List.nth tl i in (cl,parsno) + let parsno = + match CicEnvironment.get_cooked_obj uri with + C.InductiveDefinition (_,_,parsno) -> parsno | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in let (_,branches_ok) = List.fold_left - (fun (j,b) (p,(_,c,_)) -> + (fun (j,b) p -> let cons = if parameters = [] then - (C.MutConstruct (uri,cookingsno,i,j)) + (C.MutConstruct (uri,i,j,exp_named_subst)) else - (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters)) + (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in +(* (j + 1, b && +*) + (j + 1, +let res = b && R.are_convertible context (type_of_aux context p) (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons)) +in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res ) - ) (1,true) (List.combine pl cl) + ) (1,true) pl in if not branches_ok then raise (NotWellTyped "MutCase: wrong type of a branch") ; @@ -1372,6 +1491,35 @@ and type_of_aux' metasenv context t = let (_,ty,_) = List.nth fl i in ty + and check_exp_named_subst context = + let rec check_exp_named_subst_aux substs = + function + [] -> () + | ((uri,t) as subst)::tl -> + let typeofvar = + CicSubstitution.subst_vars substs (type_of_variable uri) in + (match CicEnvironment.get_cooked_obj uri with + Cic.Variable (_,Some bo,_,_) -> + raise + (NotWellTyped + "A variable with a body can not be explicit substituted") + | Cic.Variable (_,None,_,_) -> () + | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + ) ; + let typeoft = type_of_aux context t in + if CicReduction.are_convertible context typeoft typeofvar then + check_exp_named_subst_aux (substs@[subst]) tl + else + begin + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible context typeoft typeofvar) ; + fdebug := 0 ; + debug typeoft [typeofvar] ; + raise (NotWellTyped "Wrong Explicit Named Substitution") + end + in + check_exp_named_subst_aux [] + and sort_of_prod context (name,s) (t1, t2) = let module C = Cic in let t1' = CicReduction.whd context t1 in @@ -1412,17 +1560,17 @@ and type_of_aux' metasenv context t = and returns_a_coinductive context ty = let module C = Cic in match CicReduction.whd context ty with - C.MutInd (uri,cookingsno,i) -> + C.MutInd (uri,i,_) -> (*CSC: definire una funzioncina per questo codice sempre replicato *) - (match CicEnvironment.get_cooked_obj uri cookingsno with + (match CicEnvironment.get_cooked_obj uri with C.InductiveDefinition (itl,_,_) -> - let (_,is_inductive,_,cl) = List.nth itl i in + let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) ) - | C.Appl ((C.MutInd (uri,_,i))::_) -> + | C.Appl ((C.MutInd (uri,i,_))::_) -> (match CicEnvironment.get_obj uri with C.InductiveDefinition (itl,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in @@ -1476,26 +1624,26 @@ let typecheck uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked uri 0 with + match CicEnvironment.is_type_checked uri with CicEnvironment.CheckedObj _ -> () | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) Logger.log (`Start_type_checking uri) ; (match uobj with - C.Definition (_,te,ty,_) -> + C.Constant (_,Some te,ty,_) -> let _ = type_of ty in if not (R.are_convertible [] (type_of te ) ty) then raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) - | C.Axiom (_,ty,_) -> + | C.Constant (_,None,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in () - | C.CurrentProof (_,conjs,te,ty) -> + | C.CurrentProof (_,conjs,te,ty,_) -> (*CSC: bisogna controllare anche il metasenv!!! *) let _ = type_of_aux' conjs [] ty in debug (type_of_aux' conjs [] te) [] ; if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) - | C.Variable (_,bo,ty) -> + | C.Variable (_,bo,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in (match bo with @@ -1505,7 +1653,7 @@ let typecheck uri = raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) ) | C.InductiveDefinition _ -> - cooked_mutual_inductive_defs uri uobj + check_mutual_inductive_defs uri uobj ) ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index af67f1c14..a039921c2 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -43,10 +43,6 @@ aux 1 ;; - let get_cookingno uri = - UriManager.relative_depth !CicTextualParser0.current_uri uri 0 - ;; - (* Returns the first meta whose number is above the *) (* number of the higher meta. *) (*CSC: cut&pasted from proofEngine.ml *) @@ -101,19 +97,18 @@ expr2: { let uri = UriManager.string_of_uri $1 in let suff = (String.sub uri (String.length uri - 3) 3) in match suff with - "con" -> - let cookingno = get_cookingno $1 in - Const ($1,cookingno) - | "var" -> Var $1 +(*CSC: parsare anche le explicit named substitutions *) + "con" -> Const ($1,[]) + | "var" -> Var ($1,[]) | _ -> raise (InvalidSuffix suff) } | INDTYURI - { let cookingno = get_cookingno (fst $1) in - MutInd (fst $1, cookingno, snd $1) } +/*CSC: parsare anche le explicit named substitutions */ + { MutInd (fst $1, snd $1, []) } | INDCONURI { let (uri,tyno,consno) = $1 in - let cookingno = get_cookingno uri in - MutConstruct (uri, cookingno, tyno, consno) } +(*CSC: parsare anche le explicit named substitutions *) + MutConstruct (uri, tyno, consno, []) } | ID { try Rel (get_index_in_list (Name $1) !CicTextualParser0.binders) @@ -128,8 +123,7 @@ expr2: | Some term -> Hashtbl.add uri_of_id_map $1 term; term } | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY - { let cookingno = get_cookingno (fst $5) in - MutCase (fst $5, cookingno, snd $5, $7, $3, $10) } + { MutCase (fst $5, snd $5, $7, $3, $10) } | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY { try let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in @@ -137,8 +131,8 @@ expr2: with Not_found -> match Hashtbl.find uri_of_id_map $5 with - MutInd (uri,cookingno,typeno) -> - MutCase (uri, cookingno, typeno, $7, $3, $10) + MutInd (uri,typeno,_) -> + MutCase (uri, typeno, $7, $3, $10) | _ -> raise InductiveTypeURIExpected } | fixheader LCURLY exprseplist RCURLY @@ -247,11 +241,11 @@ pihead: { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; (Cic.Name $2, $4) } | expr2 ARROW - { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; - (Anonimous, $1) } + { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ; + (Anonymous, $1) } | LPAREN expr RPAREN ARROW - { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ; - (Anonimous, $2) } + { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ; + (Anonymous, $2) } ; lambdahead: LAMBDA ID COLON expr DOT @@ -283,16 +277,13 @@ substitutionlist: ; alias: ALIAS ID CONURI - { let cookingno = get_cookingno $3 in - Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) } + { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,[])) } | ALIAS ID INDTYURI - { let cookingno = get_cookingno (fst $3) in - Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) } + { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, snd $3, [])) } | ALIAS ID INDCONURI { let uri,indno,consno = $3 in - let cookingno = get_cookingno uri in - Hashtbl.add uri_of_id_map $2 - (Cic.MutConstruct (uri, cookingno, indno ,consno)) + Hashtbl.add uri_of_id_map $2 + (Cic.MutConstruct (uri, indno, consno, [])) } diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index cd1e7aa0c..66c88e60f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -103,11 +103,23 @@ let delift context metasenv l t = | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, deliftaux k outty, deliftaux k t, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, deliftaux k outty, deliftaux k t, List.map (deliftaux k) pl) | C.Fix (i, fl) -> let len = List.length fl in @@ -144,113 +156,115 @@ type substitution = (int * Cic.term) list a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -let fo_unif_new metasenv context t1 t2 = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let rec fo_unif_aux subst context metasenv t1 t2 = - match (t1, t2) with - (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let ok = - List.fold_left2 - (fun b t1 t2 -> - b && - match t1,t2 with - None,_ - | _,None -> true - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - R.are_convertible context t1' t2' - ) true ln lm - in - if ok then subst,metasenv else - raise UnificationFailed - | (C.Meta (n,l), C.Meta (m,_)) when n>m -> - fo_unif_aux subst context metasenv t2 t1 - | (C.Meta (n,l), t) - | (t, C.Meta (n,l)) -> - let subst',metasenv' = - try - let oldt = (List.assoc n subst) in - let lifted_oldt = S.lift_meta l oldt in - fo_unif_aux subst context metasenv lifted_oldt t - with Not_found -> -prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ; -List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; -prerr_endline " m=n) metasenv' in - let tyt = CicTypeChecker.type_of_aux' metasenv' context t in - fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt - | (C.Rel _, _) - | (_, C.Rel _) - | (C.Var _, _) - | (_, C.Var _) - | (C.Sort _ ,_) - | (_, C.Sort _) - | (C.Implicit, _) - | (_, C.Implicit) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in - fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in - fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_aux subst context metasenv t2 (S.subst s1 t1) - | (C.Appl l1, C.Appl l2) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_l subst metasenv = function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_aux subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> - fo_unif_aux subst context metasenv h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_aux subst context metasenv h1 h2 - in - fo_unif_l subst' metasenv' (l1,l2) - in - fo_unif_l subst metasenv (lr1, lr2) - | (C.Const _, _) - | (_, C.Const _) - | (C.MutInd _, _) - | (_, C.MutInd _) - | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> - let subst', metasenv' = - fo_unif_aux subst context metasenv outt1 outt2 in - let subst'',metasenv'' = - fo_unif_aux subst' context metasenv' t1 t2 in - List.fold_left2 - (function (subst,metasenv) -> - fo_unif_aux subst context metasenv - ) (subst'',metasenv'') pl1 pl2 - | (C.Fix _, _) - | (_, C.Fix _) - | (C.CoFix _, _) - | (_, C.CoFix _) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (_,_) -> raise UnificationFailed - in fo_unif_aux [] context metasenv t1 t2;; +let rec fo_unif_subst subst context metasenv t1 t2 = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + match (t1, t2) with + (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> + let ok = + List.fold_left2 + (fun b t1 t2 -> + b && + match t1,t2 with + None,_ + | _,None -> true + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + R.are_convertible context t1' t2' + ) true ln lm + in + if ok then subst,metasenv else raise UnificationFailed + | (C.Meta (n,l), C.Meta (m,_)) when n>m -> + fo_unif_subst subst context metasenv t2 t1 + | (C.Meta (n,l), t) + | (t, C.Meta (n,l)) -> + let subst',metasenv' = + try + let oldt = (List.assoc n subst) in + let lifted_oldt = S.lift_meta l oldt in + fo_unif_subst subst context metasenv lifted_oldt t + with Not_found -> + let t',metasenv' = delift context metasenv l t in + (n, t')::subst, metasenv' + in + let (_,_,meta_type) = + List.find (function (m,_,_) -> m=n) metasenv' in + let tyt = CicTypeChecker.type_of_aux' metasenv' context t in + fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt + | (C.Rel _, _) + | (_, C.Rel _) + | (C.Var _, _) + | (_, C.Var _) + | (C.Sort _ ,_) + | (_, C.Sort _) + | (C.Implicit, _) + | (_, C.Implicit) -> + if R.are_convertible context t1 t2 then + subst, metasenv + else + raise UnificationFailed + | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2 + | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in + fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> + let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in + fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.LetIn (_,s1,t1), t2) + | (t2, C.LetIn (_,s1,t1)) -> + fo_unif_subst subst context metasenv t2 (S.subst s1 t1) + | (C.Appl l1, C.Appl l2) -> + let lr1 = List.rev l1 in + let lr2 = List.rev l2 in + let rec fo_unif_l subst metasenv = + function + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_subst subst context metasenv h1 h2 + | ([h],l) + | (l,[h]) -> + fo_unif_subst subst context metasenv h (C.Appl (List.rev l)) + | ((h1::l1),(h2::l2)) -> + let subst', metasenv' = + fo_unif_subst subst context metasenv h1 h2 + in + fo_unif_l subst' metasenv' (l1,l2) + in + fo_unif_l subst metasenv (lr1, lr2) + | (C.Const _, _) + | (_, C.Const _) + | (C.MutInd _, _) + | (_, C.MutInd _) + | (C.MutConstruct _, _) + | (_, C.MutConstruct _) -> + if R.are_convertible context t1 t2 then + subst, metasenv + else + raise UnificationFailed + | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))-> + let subst', metasenv' = + fo_unif_subst subst context metasenv outt1 outt2 in + let subst'',metasenv'' = + fo_unif_subst subst' context metasenv' t1 t2 in + List.fold_left2 + (function (subst,metasenv) -> + fo_unif_subst subst context metasenv + ) (subst'',metasenv'') pl1 pl2 + | (C.Fix _, _) + | (_, C.Fix _) + | (C.CoFix _, _) + | (_, C.CoFix _) -> + if R.are_convertible context t1 t2 then + subst, metasenv + else + raise UnificationFailed + | (_,_) -> raise UnificationFailed +;; (*CSC: ??????????????? (* m is the index of a metavariable to restrict, k is nesting depth @@ -442,10 +456,34 @@ prerr_endline " C.Appl (he'::tl'),metasenv'' end | C.Appl _ -> assert false - | C.Const _ - | C.MutInd _ - | C.MutConstruct _ as t -> t,metasenv - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + | C.Const (uri,exp_named_subst) -> + let exp_named_subst', metasenv' = + List.fold_right + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) + in + C.Const (uri,exp_named_subst'),metasenv' + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst', metasenv' = + List.fold_right + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) + in + C.MutInd (uri,typeno,exp_named_subst'),metasenv' + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst', metasenv' = + List.fold_right + (fun (uri,t) (tl,metasenv) -> + let t',metasenv' = um_aux metasenv t in + (uri,t')::tl, metasenv' + ) exp_named_subst ([],metasenv) + in + C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv' + | C.MutCase (sp,i,outty,t,pl) -> let outty',metasenv' = um_aux metasenv outty in let t',metasenv'' = um_aux metasenv' t in let pl',metasenv''' = @@ -455,7 +493,7 @@ prerr_endline " let len = List.length fl in let liftedfl,metasenv' = @@ -536,11 +574,23 @@ let apply_subst_reducing subst meta_to_reduce t = | _,_ -> t' end | C.Appl _ -> assert false - | C.Const _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t, + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst + in + C.MutInd (uri,typeno,exp_named_subst') + | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst + in + C.MutConstruct (uri,typeno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, um_aux outty, um_aux t, List.map um_aux pl) | C.Fix (i, fl) -> let len = List.length fl in @@ -604,7 +654,7 @@ let apply_subst subst t = (* metavariables may have been restricted. *) let fo_unif metasenv context t1 t2 = prerr_endline "INIZIO FASE 1" ; flush stderr ; - let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in + let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in prerr_endline "FINE FASE 1" ; flush stderr ; let res = unwind_subst metasenv' subst_to_unwind diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 464927a2d..46f506710 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -38,12 +38,31 @@ type substitution = (int * Cic.term) list (* unifies [t1] and [t2] in a context [context]. *) (* Only the metavariables declared in [metasenv] *) (* can be used in [t1] and [t2]. *) +(* The returned substitution can be directly *) +(* withouth first unwinding it. *) val fo_unif : Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> substitution * Cic.metasenv -(* apply_subst subst t *) -(* applies the substitution [sust] to [t] *) +(* fo_unif_subst metasenv subst context t1 t2 *) +(* unifies [t1] and [t2] in a context [context] *) +(* and with [subst] as the current substitution *) +(* (i.e. unifies ([subst] [t1]) and *) +(* ([subst] [t2]) in a context *) +(* ([subst] [context]) using the metasenv *) +(* ([subst] [metasenv]) *) +(* Only the metavariables declared in [metasenv] *) +(* can be used in [t1] and [t2]. *) +(* [subst] and the substitution returned are not *) +(* unwinded. *) +(*CSC: fare un tipo unione Unwinded o ToUnwind e fare gestire la + cosa all'apply_subst!!!*) +val fo_unif_subst : + substitution -> Cic.context -> Cic.metasenv -> Cic.term -> Cic.term -> + substitution * Cic.metasenv + +(* apply_subst subst t *) +(* applies the substitution [subst] to [t] *) val apply_subst : substitution -> Cic.term -> Cic.term (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) diff --git a/helm/ocaml/getter/getter.ml b/helm/ocaml/getter/getter.ml index 894bf3ea9..c1ba01016 100644 --- a/helm/ocaml/getter/getter.ml +++ b/helm/ocaml/getter/getter.ml @@ -61,3 +61,35 @@ let register uri url = "?uri=" ^ (UriManager.string_of_uri uri) ^ "&url=" ^ url) ;; + +exception Unresolved;; +exception UnexpectedGetterOutput;; + +(* resolve_result is needed because it is not possible to raise *) +(* an exception in a pxp even-processing callback. Too bad. *) +type resolve_result = + Unknown + | Exception of exn + | Resolved of string + +let resolve uri = + (* deliver resolve request to http_getter *) + let doc = + ClientHTTP.get + (!getter_url ^ "resolve" ^ "?uri=" ^ (UriManager.string_of_uri uri)) + in + let res = ref Unknown in + Pxp_yacc.process_entity Pxp_yacc.default_config (`Entry_content []) + (Pxp_yacc.create_entity_manager ~is_document:true Pxp_yacc.default_config + (Pxp_yacc.from_string doc)) + (function + Pxp_yacc.E_start_tag ("url",["value",url],_) -> res := Resolved url + | Pxp_yacc.E_start_tag ("unresolved",[],_) -> res := Exception Unresolved + | Pxp_yacc.E_start_tag _ -> res := Exception UnexpectedGetterOutput + | _ -> () + ) ; + match !res with + Unknown -> raise UnexpectedGetterOutput + | Exception e -> raise e + | Resolved url -> url +;; diff --git a/helm/ocaml/getter/getter.mli b/helm/ocaml/getter/getter.mli index 6b1d2ca29..3fbec8070 100644 --- a/helm/ocaml/getter/getter.mli +++ b/helm/ocaml/getter/getter.mli @@ -51,3 +51,12 @@ val getxml : ?format:format -> ?patchdtd:bool -> UriManager.uri -> string (* adds an (URI -> URL) entry in the map from URIs to URLs *) val register : UriManager.uri -> string -> unit + +exception Unresolved +exception UnexpectedGetterOutput + +(* resolves an URI to its corresponding URL. *) +(* Unresolved is raised if there is no URL for the given URI. *) +(* UnexceptedGetterOutput is raised if the output of the real *) +(* getter has not the expected format. *) +val resolve: UriManager.uri -> string diff --git a/helm/ocaml/pxp/.depend b/helm/ocaml/pxp/.depend index 529d934c7..c2a1a4be6 100644 --- a/helm/ocaml/pxp/.depend +++ b/helm/ocaml/pxp/.depend @@ -1,5 +1,2 @@ -pxpUriResolver.cmi: csc_pxp_reader.cmi -csc_pxp_reader.cmo: csc_pxp_reader.cmi -csc_pxp_reader.cmx: csc_pxp_reader.cmi -pxpUriResolver.cmo: csc_pxp_reader.cmi pxpUriResolver.cmi -pxpUriResolver.cmx: csc_pxp_reader.cmx pxpUriResolver.cmi +pxpUrlResolver.cmo: pxpUrlResolver.cmi +pxpUrlResolver.cmx: pxpUrlResolver.cmi diff --git a/helm/ocaml/pxp/Makefile b/helm/ocaml/pxp/Makefile index b40081f45..40f698344 100644 --- a/helm/ocaml/pxp/Makefile +++ b/helm/ocaml/pxp/Makefile @@ -2,7 +2,7 @@ PACKAGE = pxp REQUIRES = helm-getter PREDICATES = -INTERFACE_FILES = csc_pxp_reader.mli pxpUriResolver.mli +INTERFACE_FILES = pxpUrlResolver.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/pxp/csc_pxp_reader.ml b/helm/ocaml/pxp/csc_pxp_reader.ml deleted file mode 100644 index 0b849589a..000000000 --- a/helm/ocaml/pxp/csc_pxp_reader.ml +++ /dev/null @@ -1,1014 +0,0 @@ -(* $Id$ - * ---------------------------------------------------------------------- - * PXP: The polymorphic XML parser for Objective Caml. - * Copyright by Gerd Stolpmann. See LICENSE for details. - *) - -open Pxp_types;; -exception Not_competent;; -exception Not_resolvable of exn;; - -class type resolver = - object - method init_rep_encoding : rep_encoding -> unit - method init_warner : collect_warnings -> unit - method rep_encoding : rep_encoding - method open_in : ext_id -> Lexing.lexbuf - method close_in : unit - method close_all : unit - method change_encoding : string -> unit - method clone : resolver - end -;; - - -class virtual resolve_general - = - object (self) - val mutable internal_encoding = `Enc_utf8 - - val mutable encoding = `Enc_utf8 - val mutable encoding_requested = false - - val mutable warner = new drop_warnings - - val mutable enc_initialized = false - val mutable wrn_initialized = false - - val mutable clones = [] - - method init_rep_encoding e = - internal_encoding <- e; - enc_initialized <- true; - - method init_warner w = - warner <- w; - wrn_initialized <- true; - - method rep_encoding = (internal_encoding :> rep_encoding) - -(* - method clone = - ( {< encoding = `Enc_utf8; - encoding_requested = false; - >} - : # resolver :> resolver ) -*) - - method private warn (k:int) = - (* Called if a character not representable has been found. - * k is the character code. - *) - if k < 0xd800 or (k >= 0xe000 & k <= 0xfffd) or - (k >= 0x10000 & k <= 0x10ffff) then begin - warner # warn ("Code point cannot be represented: " ^ string_of_int k); - end - else - raise (WF_error("Code point " ^ string_of_int k ^ - " outside the accepted range of code points")) - - - method private autodetect s = - (* s must be at least 4 bytes long. The slot 'encoding' is - * set to: - * "UTF-16-BE": UTF-16/UCS-2 encoding big endian - * "UTF-16-LE": UTF-16/UCS-2 encoding little endian - * "UTF-8": UTF-8 encoding - *) - if String.length s < 4 then - encoding <- `Enc_utf8 - else if String.sub s 0 2 = "\254\255" then - encoding <- `Enc_utf16 - (* Note: Netconversion.recode will detect the big endianess, too *) - else if String.sub s 0 2 = "\255\254" then - encoding <- `Enc_utf16 - (* Note: Netconversion.recode will detect the little endianess, too *) - else - encoding <- `Enc_utf8 - - - method private virtual next_string : string -> int -> int -> int - method private virtual init_in : ext_id -> unit - method virtual close_in : unit - - method close_all = - List.iter (fun r -> r # close_in) clones - - method open_in xid = - assert(enc_initialized && wrn_initialized); - - encoding <- `Enc_utf8; - encoding_requested <- false; - self # init_in xid; (* may raise Not_competent *) - (* init_in: may already set 'encoding' *) - - let buffer_max = 512 in - let buffer = String.make buffer_max ' ' in - let buffer_len = ref 0 in - let buffer_end = ref false in - let fillup () = - if not !buffer_end & !buffer_len < buffer_max then begin - let l = - self # next_string buffer !buffer_len (buffer_max - !buffer_len) in - if l = 0 then - buffer_end := true - else begin - buffer_len := !buffer_len + l - end - end - in - let consume n = - let l = !buffer_len - n in - String.blit buffer n buffer 0 l; - buffer_len := l - in - - fillup(); - if not encoding_requested then self # autodetect buffer; - - Lexing.from_function - (fun s n -> - (* TODO: if encoding = internal_encoding, it is possible to - * avoid copying buffer to s because s can be directly used - * as buffer. - *) - - fillup(); - if !buffer_len = 0 then - 0 - else begin - let m_in = !buffer_len in - let m_max = if encoding_requested then n else 1 in - let n_in, n_out, encoding' = - if encoding = (internal_encoding : rep_encoding :> encoding) && - encoding_requested - then begin - (* Special case encoding = internal_encoding *) - String.blit buffer 0 s 0 m_in; - m_in, m_in, encoding - end - else - Netconversion.recode - ~in_enc:encoding - ~in_buf:buffer - ~in_pos:0 - ~in_len:m_in - ~out_enc:(internal_encoding : rep_encoding :> encoding) - ~out_buf:s - ~out_pos:0 - ~out_len:n - ~max_chars:m_max - ~subst:(fun k -> self # warn k; "") - in - if n_in = 0 then - (* An incomplete character at the end of the stream: *) - raise Netconversion.Malformed_code; - (* failwith "Badly encoded character"; *) - encoding <- encoding'; - consume n_in; - assert(n_out <> 0); - n_out - end) - - method change_encoding enc = - if not encoding_requested then begin - if enc <> "" then begin - match Netconversion.encoding_of_string enc with - `Enc_utf16 -> - (match encoding with - (`Enc_utf16_le | `Enc_utf16_be) -> () - | `Enc_utf16 -> assert false - | _ -> - raise(WF_error "Encoding of data stream and encoding declaration mismatch") - ) - | e -> - encoding <- e - end; - (* else: the autodetected encoding counts *) - encoding_requested <- true; - end; - end -;; - - -class resolve_read_any_channel ?(close=close_in) ~channel_of_id () = - object (self) - inherit resolve_general as super - - val f_open = channel_of_id - val mutable current_channel = None - val close = close - - method private init_in (id:ext_id) = - if current_channel <> None then - failwith "Pxp_reader.resolve_read_any_channel # init_in"; - let ch, enc_opt = f_open id in (* may raise Not_competent *) - begin match enc_opt with - None -> () - | Some enc -> encoding <- enc; encoding_requested <- true - end; - current_channel <- Some ch; - - method private next_string s ofs len = - match current_channel with - None -> failwith "Pxp_reader.resolve_read_any_channel # next_string" - | Some ch -> - input ch s ofs len - - method close_in = - match current_channel with - None -> () - | Some ch -> - close ch; - current_channel <- None - - method clone = - let c = new resolve_read_any_channel - ?close:(Some close) ~channel_of_id:f_open () in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - (c :> resolver) - - end -;; - - -class resolve_read_this_channel1 is_stale ?id ?fixenc ?close ch = - - let getchannel = ref (fun xid -> assert false) in - - object (self) - inherit resolve_read_any_channel - ?close - ~channel_of_id:(fun xid -> !getchannel xid) - () - as super - - val mutable is_stale = is_stale - (* The channel can only be read once. To avoid that the channel - * is opened several times, the flag 'is_stale' is set after the - * first time. - *) - - val fixid = id - val fixenc = fixenc - val fixch = ch - - initializer - getchannel := self # getchannel - - method private getchannel xid = - begin match fixid with - None -> () - | Some bound_xid -> - if xid <> bound_xid then raise Not_competent - end; - ch, fixenc - - method private init_in (id:ext_id) = - if is_stale then - raise Not_competent - else begin - super # init_in id; - is_stale <- true - end - - method close_in = - current_channel <- None - - method clone = - let c = new resolve_read_this_channel1 - is_stale - ?id:fixid ?fixenc:fixenc ?close:(Some close) fixch - in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - (c :> resolver) - - end -;; - - -class resolve_read_this_channel = - resolve_read_this_channel1 false -;; - - -class resolve_read_any_string ~string_of_id () = - object (self) - inherit resolve_general as super - - val f_open = string_of_id - val mutable current_string = None - val mutable current_pos = 0 - - method private init_in (id:ext_id) = - if current_string <> None then - failwith "Pxp_reader.resolve_read_any_string # init_in"; - let s, enc_opt = f_open id in (* may raise Not_competent *) - begin match enc_opt with - None -> () - | Some enc -> encoding <- enc; encoding_requested <- true - end; - current_string <- Some s; - current_pos <- 0; - - method private next_string s ofs len = - match current_string with - None -> failwith "Pxp_reader.resolve_read_any_string # next_string" - | Some str -> - let l = min len (String.length str - current_pos) in - String.blit str current_pos s ofs l; - current_pos <- current_pos + l; - l - - method close_in = - match current_string with - None -> () - | Some _ -> - current_string <- None - - method clone = - let c = new resolve_read_any_string ~string_of_id:f_open () in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - (c :> resolver) - end -;; - - -class resolve_read_this_string1 is_stale ?id ?fixenc str = - - let getstring = ref (fun xid -> assert false) in - - object (self) - inherit resolve_read_any_string (fun xid -> !getstring xid) () as super - - val is_stale = is_stale - (* For some reasons, it is not allowed to open a clone of the resolver - * a second time when the original resolver is already open. - *) - - val fixid = id - val fixenc = fixenc - val fixstr = str - - initializer - getstring := self # getstring - - method private getstring xid = - begin match fixid with - None -> () - | Some bound_xid -> - if xid <> bound_xid then raise Not_competent - end; - fixstr, fixenc - - - method private init_in (id:ext_id) = - if is_stale then - raise Not_competent - else - super # init_in id - - method clone = - let c = new resolve_read_this_string1 - (is_stale or current_string <> None) - ?id:fixid ?fixenc:fixenc fixstr - in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - (c :> resolver) - end -;; - - -class resolve_read_this_string = - resolve_read_this_string1 false -;; - - -class resolve_read_url_channel - ?(base_url = Neturl.null_url) - ?close - ~url_of_id - ~channel_of_url - () - - : resolver - = - - let getchannel = ref (fun xid -> assert false) in - - object (self) - inherit resolve_read_any_channel - ?close - ~channel_of_id:(fun xid -> !getchannel xid) - () - as super - - val base_url = base_url - val mutable own_url = Neturl.null_url - - val url_of_id = url_of_id - val channel_of_url = channel_of_url - - - initializer - getchannel := self # getchannel - - method private getchannel xid = - let rel_url = url_of_id xid in (* may raise Not_competent *) - - try - (* Now compute the absolute URL: *) - let abs_url = - if Neturl.url_provides ~scheme:true rel_url then - rel_url - else - Neturl.apply_relative_url base_url rel_url in - (* may raise Malformed_URL *) - - (* Simple check whether 'abs_url' is really absolute: *) - if not(Neturl.url_provides ~scheme:true abs_url) - then raise Not_competent; - - own_url <- abs_url; - (* FIXME: Copy 'abs_url' ? *) - - (* Get and return the channel: *) - channel_of_url xid abs_url (* may raise Not_competent *) - with - Neturl.Malformed_URL -> raise (Not_resolvable Neturl.Malformed_URL) - | Not_competent -> raise (Not_resolvable Not_found) - - method clone = - let c = - new resolve_read_url_channel - ?base_url:(Some own_url) - ?close:(Some close) - ~url_of_id:url_of_id - ~channel_of_url:channel_of_url - () - in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - (c :> resolve_read_url_channel) - end -;; - - -type spec = [ `Not_recognized | `Allowed | `Required ] - -class resolve_as_file - ?(file_prefix = (`Allowed :> spec)) - ?(host_prefix = (`Allowed :> spec)) - ?(system_encoding = `Enc_utf8) - ?(map_private_id = (fun _ -> raise Not_competent)) - ?(open_private_id = (fun _ -> raise Not_competent)) - () - = - - let url_syntax = - let enable_if = - function - `Not_recognized -> Neturl.Url_part_not_recognized - | `Allowed -> Neturl.Url_part_allowed - | `Required -> Neturl.Url_part_required - in - { Neturl.null_url_syntax with - Neturl.url_enable_scheme = enable_if file_prefix; - Neturl.url_enable_host = enable_if host_prefix; - Neturl.url_enable_path = Neturl.Url_part_required; - Neturl.url_accepts_8bits = true; - } - in - - let base_url_syntax = - { Neturl.null_url_syntax with - Neturl.url_enable_scheme = Neturl.Url_part_required; - Neturl.url_enable_host = Neturl.Url_part_allowed; - Neturl.url_enable_path = Neturl.Url_part_required; - Neturl.url_accepts_8bits = true; - } - in - - let default_base_url = - Neturl.make_url - ~scheme: "file" - ~host: "" - ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) - base_url_syntax - in - - let file_url_of_id xid = - let file_url_of_sysname sysname = - (* By convention, we can assume that sysname is a URL conforming - * to RFC 1738 with the exception that it may contain non-ASCII - * UTF-8 characters. - *) - try - Neturl.url_of_string url_syntax sysname - (* may raise Malformed_URL *) - with - Neturl.Malformed_URL -> raise Not_competent - in - let url = - match xid with - Anonymous -> raise Not_competent - | Public (_,sysname) -> if sysname <> "" then file_url_of_sysname sysname - else raise Not_competent - | System sysname -> file_url_of_sysname sysname - | Private pid -> map_private_id pid - in - let scheme = - try Neturl.url_scheme url with Not_found -> "file" in - let host = - try Neturl.url_host url with Not_found -> "" in - - if scheme <> "file" then raise Not_competent; - if host <> "" && host <> "localhost" then raise Not_competent; - - url - in - - let channel_of_file_url xid url = - match xid with - Private pid -> open_private_id pid - | _ -> - ( try - let path_utf8 = - try Neturl.join_path (Neturl.url_path ~encoded:false url) - with Not_found -> raise Not_competent - in - - let path = - Netconversion.recode_string - ~in_enc: `Enc_utf8 - ~out_enc: system_encoding - path_utf8 in - (* May raise Malformed_code *) - - open_in_bin path, None - (* May raise Sys_error *) - - with - | Netconversion.Malformed_code -> assert false - (* should not happen *) - | Sys_error _ as e -> - raise (Not_resolvable e) - ) - in - - resolve_read_url_channel - ~base_url: default_base_url - ~url_of_id: file_url_of_id - ~channel_of_url: channel_of_file_url - () -;; - - -let make_file_url ?(system_encoding = `Enc_utf8) ?(enc = `Enc_utf8) filename = - let utf8_filename = - Netconversion.recode_string - ~in_enc: enc - ~out_enc: `Enc_utf8 - filename - in - - let utf8_abs_filename = - if utf8_filename <> "" && utf8_filename.[0] = '/' then - utf8_filename - else - let cwd = Sys.getcwd() in - let cwd_utf8 = - Netconversion.recode_string - ~in_enc: system_encoding - ~out_enc: `Enc_utf8 in - cwd ^ "/" ^ utf8_filename - in - - let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in - let url = Neturl.make_url - ~scheme:"file" - ~host:"localhost" - ~path:(Neturl.split_path utf8_abs_filename) - syntax - in - url -;; - - -class lookup_public_id (catalog : (string * resolver) list) = - let norm_catalog = - List.map (fun (id,s) -> Pxp_aux.normalize_public_id id, s) catalog in -( object (self) - val cat = norm_catalog - val mutable internal_encoding = `Enc_utf8 - val mutable warner = new drop_warnings - val mutable active_resolver = None - - method init_rep_encoding enc = - internal_encoding <- enc - - method init_warner w = - warner <- w; - - method rep_encoding = internal_encoding - (* CAUTION: This may not be the truth! *) - - method open_in xid = - - if active_resolver <> None then failwith "Pxp_reader.lookup_* # open_in"; - - let r = - match xid with - Public(pubid,_) -> - begin - (* Search pubid in catalog: *) - try - let norm_pubid = Pxp_aux.normalize_public_id pubid in - List.assoc norm_pubid cat - with - Not_found -> - raise Not_competent - end - | _ -> - raise Not_competent - in - - let r' = r # clone in - r' # init_rep_encoding internal_encoding; - r' # init_warner warner; - let lb = r' # open_in xid in (* may raise Not_competent *) - active_resolver <- Some r'; - lb - - method close_in = - match active_resolver with - None -> () - | Some r -> r # close_in; - active_resolver <- None - - method close_all = - self # close_in - - method change_encoding (enc:string) = - match active_resolver with - None -> failwith "Pxp_reader.lookup_* # change_encoding" - | Some r -> r # change_encoding enc - - method clone = - let c = new lookup_public_id cat in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - c - end : resolver ) -;; - - -let lookup_public_id_as_file ?(fixenc:encoding option) catalog = - let ch_of_id filename id = - let ch = open_in_bin filename in (* may raise Sys_error *) - ch, fixenc - in - let catalog' = - List.map - (fun (id,s) -> - (id, new resolve_read_any_channel (ch_of_id s) ()) - ) - catalog - in - new lookup_public_id catalog' -;; - - -let lookup_public_id_as_string ?(fixenc:encoding option) catalog = - let catalog' = - List.map - (fun (id,s) -> - (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) - ) - catalog - in - new lookup_public_id catalog' -;; - - -class lookup_system_id (catalog : (string * resolver) list) = -( object (self) - val cat = catalog - val mutable internal_encoding = `Enc_utf8 - val mutable warner = new drop_warnings - val mutable active_resolver = None - - method init_rep_encoding enc = - internal_encoding <- enc - - method init_warner w = - warner <- w; - - method rep_encoding = internal_encoding - (* CAUTION: This may not be the truth! *) - - - method open_in xid = - - if active_resolver <> None then failwith "Pxp_reader.lookup_system_id # open_in"; - - let lookup sysid = - try - List.assoc sysid cat - with - Not_found -> - raise Not_competent - in - - let r = - match xid with - System sysid -> lookup sysid - | Public(_,sysid) -> lookup sysid - | _ -> raise Not_competent - in - - let r' = r # clone in - r' # init_rep_encoding internal_encoding; - r' # init_warner warner; - let lb = r' # open_in xid in (* may raise Not_competent *) - active_resolver <- Some r'; - lb - - - method close_in = - match active_resolver with - None -> () - | Some r -> r # close_in; - active_resolver <- None - - method close_all = - self # close_in - - method change_encoding (enc:string) = - match active_resolver with - None -> failwith "Pxp_reader.lookup_system # change_encoding" - | Some r -> r # change_encoding enc - - method clone = - let c = new lookup_system_id cat in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - c - end : resolver) -;; - - -let lookup_system_id_as_file ?(fixenc:encoding option) catalog = - let ch_of_id filename id = - let ch = open_in_bin filename in (* may raise Sys_error *) - ch, fixenc - in - let catalog' = - List.map - (fun (id,s) -> - (id, new resolve_read_any_channel (ch_of_id s) ()) - ) - catalog - in - new lookup_system_id catalog' -;; - - -let lookup_system_id_as_string ?(fixenc:encoding option) catalog = - let catalog' = - List.map - (fun (id,s) -> - (id, new resolve_read_any_string (fun _ -> s, fixenc) ()) - ) - catalog - in - new lookup_system_id catalog' -;; - - -type combination_mode = - Public_before_system - | System_before_public -;; - - -class combine ?prefer ?(mode = Public_before_system) rl = - object (self) - val prefered_resolver = prefer - val mode = mode - val resolvers = (rl : resolver list) - val mutable internal_encoding = `Enc_utf8 - val mutable warner = new drop_warnings - val mutable active_resolver = None - val mutable clones = [] - - method init_rep_encoding enc = - List.iter - (fun r -> r # init_rep_encoding enc) - rl; - internal_encoding <- enc - - method init_warner w = - List.iter - (fun r -> r # init_warner w) - rl; - warner <- w; - - method rep_encoding = internal_encoding - (* CAUTION: This may not be the truth! *) - - method open_in xid = - let rec find_competent_resolver_for xid' rl = - match rl with - r :: rl' -> - begin try - r, (r # open_in xid') - with - Not_competent -> find_competent_resolver_for xid' rl' - end; - | [] -> - raise Not_competent - in - - let find_competent_resolver rl = - match xid with - Public(pubid,sysid) -> - ( match mode with - Public_before_system -> - ( try - find_competent_resolver_for(Public(pubid,"")) rl - with - Not_competent -> - find_competent_resolver_for(System sysid) rl - ) - | System_before_public -> - ( try - find_competent_resolver_for(System sysid) rl - with - Not_competent -> - find_competent_resolver_for(Public(pubid,"")) rl - ) - ) - | other -> - find_competent_resolver_for other rl - in - - if active_resolver <> None then failwith "Pxp_reader.combine # open_in"; - let r, lb = - match prefered_resolver with - None -> find_competent_resolver resolvers - | Some r -> find_competent_resolver (r :: resolvers) - in - active_resolver <- Some r; - lb - - method close_in = - match active_resolver with - None -> () - | Some r -> r # close_in; - active_resolver <- None - - method close_all = - List.iter (fun r -> r # close_in) clones - - method change_encoding (enc:string) = - match active_resolver with - None -> failwith "Pxp_reader.combine # change_encoding" - | Some r -> r # change_encoding enc - - method clone = - let c = - match active_resolver with - None -> - new combine ?prefer:None ?mode:(Some mode) - (List.map (fun q -> q # clone) resolvers) - | Some r -> - let r' = r # clone in - new combine - ?prefer:(Some r') - ?mode:(Some mode) - (List.map - (fun q -> if q == r then r' else q # clone) - resolvers) - in - c # init_rep_encoding internal_encoding; - c # init_warner warner; - clones <- c :: clones; - c - end - - - -(* ====================================================================== - * History: - * - * $Log$ - * Revision 1.2 2002/01/29 14:44:29 sacerdot - * Ported to ocaml-3.04. - * - * Revision 1.1 2001/11/26 18:28:28 sacerdot - * HELM OCaml libraries with findlib support. - * - * Revision 1.1 2001/10/24 15:33:16 sacerdot - * New procedure to create metadata committed and old procedure removed. - * The new procedure is based on ocaml code and builds metadata for both - * forward and backward pointers. The old one was based on a stylesheet. - * - * Revision 1.16 2001/07/01 09:46:40 gerd - * Fix: resolve_read_url_channel does not use the base_url if - * the current URL is already absolute - * - * Revision 1.15 2001/07/01 08:35:23 gerd - * Instead of the ~auto_close argument, there is now a - * ~close argument for several functions/classes. This allows some - * additional action when the resolver is closed. - * - * Revision 1.14 2001/06/14 23:28:02 gerd - * Fix: class combine works now with private IDs. - * - * Revision 1.13 2001/04/22 14:16:48 gerd - * resolve_as_file: you can map private IDs to arbitrary channels. - * resolve_read_url_channel: changed type of the channel_of_url - * argument (ext_id is also passed) - * More examples and documentation. - * - * Revision 1.12 2001/04/21 17:40:48 gerd - * Bugfix in 'combine' - * - * Revision 1.11 2001/04/03 20:22:44 gerd - * New resolvers for catalogs of PUBLIC and SYSTEM IDs. - * Improved "combine": PUBLIC and SYSTEM IDs are handled - * separately. - * Rewritten from_file: Is now a simple application of the - * Pxp_reader classes and functions. (The same has still to be done - * for from_channel!) - * - * Revision 1.10 2001/02/01 20:38:49 gerd - * New support for PUBLIC identifiers. - * - * Revision 1.9 2000/08/14 22:24:55 gerd - * Moved the module Pxp_encoding to the netstring package under - * the new name Netconversion. - * - * Revision 1.8 2000/07/16 18:31:09 gerd - * The exception Illegal_character has been dropped. - * - * Revision 1.7 2000/07/09 15:32:01 gerd - * Fix in resolve_this_channel, resolve_this_string - * - * Revision 1.6 2000/07/09 01:05:33 gerd - * New methode 'close_all' that closes the clones, too. - * - * Revision 1.5 2000/07/08 16:24:56 gerd - * Introduced the exception 'Not_resolvable' to indicate that - * 'combine' should not try the next resolver of the list. - * - * Revision 1.4 2000/07/06 23:04:46 gerd - * Quick fix for 'combine': The active resolver is "prefered", - * but the other resolvers are also used. - * - * Revision 1.3 2000/07/06 21:43:45 gerd - * Fix: Public(_,name) is now treated as System(name) if - * name is non-empty. - * - * Revision 1.2 2000/07/04 22:13:30 gerd - * Implemented the new API rev. 1.2 of pxp_reader.mli. - * - * Revision 1.1 2000/05/29 23:48:38 gerd - * Changed module names: - * Markup_aux into Pxp_aux - * Markup_codewriter into Pxp_codewriter - * Markup_document into Pxp_document - * Markup_dtd into Pxp_dtd - * Markup_entity into Pxp_entity - * Markup_lexer_types into Pxp_lexer_types - * Markup_reader into Pxp_reader - * Markup_types into Pxp_types - * Markup_yacc into Pxp_yacc - * See directory "compatibility" for (almost) compatible wrappers emulating - * Markup_document, Markup_dtd, Markup_reader, Markup_types, and Markup_yacc. - * - * ====================================================================== - * Old logs from markup_reader.ml: - * - * Revision 1.3 2000/05/29 21:14:57 gerd - * Changed the type 'encoding' into a polymorphic variant. - * - * Revision 1.2 2000/05/20 20:31:40 gerd - * Big change: Added support for various encodings of the - * internal representation. - * - * Revision 1.1 2000/03/13 23:41:44 gerd - * Initial revision; this code was formerly part of Markup_entity. - * - * - *) diff --git a/helm/ocaml/pxp/csc_pxp_reader.mli b/helm/ocaml/pxp/csc_pxp_reader.mli deleted file mode 100644 index 2d103b371..000000000 --- a/helm/ocaml/pxp/csc_pxp_reader.mli +++ /dev/null @@ -1,46 +0,0 @@ -exception Not_competent -exception Not_resolvable of exn -class type resolver = - object - method change_encoding : string -> unit - method clone : resolver - method close_all : unit - method close_in : unit - method init_rep_encoding : Pxp_types.rep_encoding -> unit - method init_warner : Pxp_types.collect_warnings -> unit - method open_in : Pxp_types.ext_id -> Lexing.lexbuf - method rep_encoding : Pxp_types.rep_encoding - end -class resolve_read_url_channel : - ?base_url:Neturl.url -> - ?close:(in_channel -> unit) -> - url_of_id:(Pxp_types.ext_id -> Neturl.url) -> - channel_of_url:(Pxp_types.ext_id -> - Neturl.url -> in_channel * Pxp_types.encoding option) -> - unit -> resolver -type spec = [ `Not_recognized | `Allowed | `Required] -val make_file_url : - ?system_encoding:Netconversion.encoding -> - ?enc:Netconversion.encoding -> string -> Neturl.url -type combination_mode = Public_before_system | System_before_public -class combine : - ?prefer:resolver -> - ?mode:combination_mode -> - resolver list -> - object - val mutable active_resolver : resolver option - val mutable clones : combine list - val mutable internal_encoding : Pxp_types.rep_encoding - val mode : combination_mode - val prefered_resolver : resolver option - val resolvers : resolver list - val mutable warner : Pxp_types.drop_warnings - method change_encoding : string -> unit - method clone : combine - method close_all : unit - method close_in : unit - method init_rep_encoding : Pxp_types.rep_encoding -> unit - method init_warner : Pxp_types.collect_warnings -> unit - method open_in : Pxp_types.ext_id -> Lexing.lexbuf - method rep_encoding : Pxp_types.rep_encoding - end diff --git a/helm/ocaml/pxp/pxpUriResolver.ml b/helm/ocaml/pxp/pxpUriResolver.ml deleted file mode 100644 index 1e2fec918..000000000 --- a/helm/ocaml/pxp/pxpUriResolver.ml +++ /dev/null @@ -1,266 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 11/10/2000 *) -(* *) -(* *) -(******************************************************************************) - -let resolve s = - let starts_with s s' = - if String.length s < String.length s' then - false - else - (String.sub s 0 (String.length s')) = s' - in - if starts_with s "http:" then - ClientHTTP.get_and_save_to_tmp s - else - s -;; - -(*PXP 1.0 -let url_syntax = - let enable_if = - function - `Not_recognized -> Neturl.Url_part_not_recognized - | `Allowed -> Neturl.Url_part_allowed - | `Required -> Neturl.Url_part_required - in - { Neturl.null_url_syntax with - Neturl.url_enable_scheme = enable_if `Allowed; - Neturl.url_enable_host = enable_if `Allowed; - Neturl.url_enable_path = Neturl.Url_part_required; - Neturl.url_accepts_8bits = true; - } -;; - -exception Unexpected;; (* Added when porting the file to PXP 1.1 *) - -let file_url_of_id xid = - let file_url_of_sysname sysname = - (* By convention, we can assume that sysname is a URL conforming - * to RFC 1738 with the exception that it may contain non-ASCII - * UTF-8 characters. - *) - try - Neturl.url_of_string url_syntax sysname - (* may raise Malformed_URL *) - with - Neturl.Malformed_URL -> raise Pxp_reader.Not_competent - in - let url = - match xid with - Pxp_types.Anonymous -> raise Pxp_reader.Not_competent - | Pxp_types.Public (_,sysname) -> - let sysname = resolve sysname in - if sysname <> "" then file_url_of_sysname sysname - else raise Pxp_reader.Not_competent - | Pxp_types.System sysname -> - let sysname = resolve sysname in - file_url_of_sysname sysname - | Pxp_types.Private pid -> raise Unexpected - in - let scheme = - try Neturl.url_scheme url with Not_found -> "file" in - let host = - try Neturl.url_host url with Not_found -> "" in - - if scheme <> "file" then raise Pxp_reader.Not_competent; - if host <> "" && host <> "localhost" then raise Pxp_reader.Not_competent; - - url -;; - -let from_file ?system_encoding utf8_filename = - - let r = - new Pxp_reader.resolve_as_file - ?system_encoding:system_encoding - ~url_of_id:file_url_of_id - () - in - - let utf8_abs_filename = - if utf8_filename <> "" && utf8_filename.[0] = '/' then - utf8_filename - else - Sys.getcwd() ^ "/" ^ utf8_filename - in - - let syntax = { Neturl.ip_url_syntax with Neturl.url_accepts_8bits = true } in - let url = Neturl.make_url - ~scheme:"file" - ~host:"localhost" - ~path:(Neturl.split_path utf8_abs_filename) - syntax - in - - let xid = Pxp_types.System (Neturl.string_of_url url) in - - - Pxp_yacc.ExtID(xid, r) -;; -*) - -(*PXP 1.1*) -(* csc_pxp_reader.ml is an exact copy of PXP pxp_reader.ml *) -(* The only reason is to loosen the interface *) - -class resolve_as_file - ?(file_prefix = (`Allowed :> Csc_pxp_reader.spec)) - ?(host_prefix = (`Allowed :> Csc_pxp_reader.spec)) - ?(system_encoding = `Enc_utf8) - ?(map_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) - ?(open_private_id = (fun _ -> raise Csc_pxp_reader.Not_competent)) - () - = - - let url_syntax = - let enable_if = - function - `Not_recognized -> Neturl.Url_part_not_recognized - | `Allowed -> Neturl.Url_part_allowed - | `Required -> Neturl.Url_part_required - in - { Neturl.null_url_syntax with - Neturl.url_enable_scheme = enable_if file_prefix; - Neturl.url_enable_host = enable_if host_prefix; - Neturl.url_enable_path = Neturl.Url_part_required; - Neturl.url_accepts_8bits = true; - } - in - - let base_url_syntax = - { Neturl.null_url_syntax with - Neturl.url_enable_scheme = Neturl.Url_part_required; - Neturl.url_enable_host = Neturl.Url_part_allowed; - Neturl.url_enable_path = Neturl.Url_part_required; - Neturl.url_accepts_8bits = true; - } - in - - let default_base_url = - Neturl.make_url - ~scheme: "file" - ~host: "" - ~path: (Neturl.split_path (Sys.getcwd() ^ "/")) - base_url_syntax - in - - let file_url_of_id xid = - let module P = Csc_pxp_reader in - let module T = Pxp_types in - let file_url_of_sysname sysname = - (* By convention, we can assume that sysname is a URL conforming - * to RFC 1738 with the exception that it may contain non-ASCII - * UTF-8 characters. - *) - try - Neturl.url_of_string url_syntax sysname - (* may raise Malformed_URL *) - with - Neturl.Malformed_URL -> raise P.Not_competent - in - let url = - match xid with - T.Anonymous -> raise P.Not_competent - | T.Public (_,sysname) -> let sysname = resolve sysname in - if sysname <> "" then file_url_of_sysname sysname - else raise P.Not_competent - | T.System sysname -> let sysname = resolve sysname in - file_url_of_sysname sysname - | T.Private pid -> map_private_id pid - in - let scheme = - try Neturl.url_scheme url with Not_found -> "file" in - let host = - try Neturl.url_host url with Not_found -> "" in - - if scheme <> "file" then raise P.Not_competent; - if host <> "" && host <> "localhost" then raise P.Not_competent; - - url - in - - let channel_of_file_url xid url = - let module P = Csc_pxp_reader in - let module T = Pxp_types in - match xid with - T.Private pid -> open_private_id pid - | _ -> - ( try - let path_utf8 = - try Neturl.join_path (Neturl.url_path ~encoded:false url) - with Not_found -> raise P.Not_competent - in - - let path = - Netconversion.recode_string - ~in_enc: `Enc_utf8 - ~out_enc: system_encoding - path_utf8 in - (* May raise Malformed_code *) - - open_in_bin path, None - (* May raise Sys_error *) - - with - | Netconversion.Malformed_code -> assert false - (* should not happen *) - | Sys_error _ as e -> - raise (P.Not_resolvable e) - ) - in - - Csc_pxp_reader.resolve_read_url_channel - ~base_url: default_base_url - ~url_of_id: file_url_of_id - ~channel_of_url: channel_of_file_url - () -;; - -let from_file ?(alt = []) ?system_encoding ?enc utf8_filename = - let r = - new resolve_as_file - ?system_encoding:system_encoding - () - in - - let url = Csc_pxp_reader.make_file_url - ?system_encoding - ?enc - utf8_filename in - - let xid = Pxp_types.System (Neturl.string_of_url url) in - - Pxp_yacc.ExtID(xid, new Csc_pxp_reader.combine (r :: alt)) -;; - diff --git a/helm/ocaml/pxp/pxpUriResolver.mli b/helm/ocaml/pxp/pxpUriResolver.mli deleted file mode 100644 index d2a1210aa..000000000 --- a/helm/ocaml/pxp/pxpUriResolver.mli +++ /dev/null @@ -1,4 +0,0 @@ -val from_file : - ?alt:Csc_pxp_reader.resolver list -> - ?system_encoding:Netconversion.encoding -> - ?enc:Netconversion.encoding -> string -> Pxp_yacc.source diff --git a/helm/ocaml/pxp/pxpUrlResolver.ml b/helm/ocaml/pxp/pxpUrlResolver.ml new file mode 100644 index 000000000..89d540e62 --- /dev/null +++ b/helm/ocaml/pxp/pxpUrlResolver.ml @@ -0,0 +1,43 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* This resolver uses ClientHTTP to download the files from the Web *) +let url_resolver = + let url_of_id = + function + Pxp_types.System url -> + let http = Hashtbl.find Neturl.common_url_syntax "http" in + Neturl.url_of_string http url + | _ -> raise Pxp_reader.Not_competent + in + let channel_of_url _ url = + let file = ClientHTTP.get_and_save_to_tmp (Neturl.string_of_url url) in + let ch = open_in file in + Unix.unlink file ; + ch,None + in + new Pxp_reader.resolve_read_url_channel + ~url_of_id ~channel_of_url () +;; diff --git a/helm/ocaml/pxp/pxpUrlResolver.mli b/helm/ocaml/pxp/pxpUrlResolver.mli new file mode 100644 index 000000000..07ac2fb95 --- /dev/null +++ b/helm/ocaml/pxp/pxpUrlResolver.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* This resolver uses ClientHTTP to download the files from the Web *) +val url_resolver : Pxp_reader.resolver diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index f45e65bf3..9f969fdd1 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -141,3 +141,13 @@ let annuri_of_uri uri = let uri_is_annuri uri = Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 ;; + +let bodyuri_of_uri uri = + let struri = string_of_uri uri in + if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then + let newuri = Array.copy uri in + newuri.(Array.length uri - 2) <- struri ^ ".body" ; + Some newuri + else + None +;; diff --git a/helm/ocaml/urimanager/uriManager.mli b/helm/ocaml/urimanager/uriManager.mli index 2cdd27e3d..9a702605e 100644 --- a/helm/ocaml/urimanager/uriManager.mli +++ b/helm/ocaml/urimanager/uriManager.mli @@ -49,3 +49,7 @@ val annuri_of_uri : uri -> uri (* given an uri, tells if it refers to an annotation *) val uri_is_annuri : uri -> bool + +(* given an uri of a constant, it gives back the uri of its body *) +(* it gives back None if the uri refers to a Variable or MutualInductiveType *) +val bodyuri_of_uri : uri -> uri option