(* 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
| 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 *)
| 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 =
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 *)
| 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
class warner =
object
method warn w =
- print_endline ("WARNING: " ^ w) ;
+ prerr_endline ("WARNING: " ^ w) ;
(raise Warnings : unit)
end
;;
(* 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)
;;
(******************************************************************************)
(* 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
(* 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)
;;
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)
;;
(* 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)
;;
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
(* 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
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
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)
;;
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
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 =
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 = {< >}
(* 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
;;
inherit cic_term
- method to_cic_term = raise (IllFormedXml 6)
+ method to_cic_term _ = raise (IllFormedXml 6)
end
;;
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
;;
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")
(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
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")
(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
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
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
;;
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")
(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
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
;;
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
;;
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
[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
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
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
;;
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
;;
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 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
;;
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
;;
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
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
;;
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
;;
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. *)
"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)) ;
(* 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
* 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
| 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
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,
(* *)
(******************************************************************************)
-(* 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
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
[< 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 ;
| 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
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 [<>]
>]
;;
["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 -> [<>]
) ;
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 ;
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
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 ->
| 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
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 ;
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
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
;;
-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 \
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
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
(* *)
(******************************************************************************)
+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;;
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
;;
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
;;
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 *)
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 *)
(* 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
+;;
(* 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 *)
(* 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
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
| 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
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 *)
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 " ; "
| 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) ->
(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
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 =
(*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 ""
;;
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 ->
"\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 ""
;;
*)
exception WrongUriToInductiveDefinition
-exception ReferenceToDefinition
-exception ReferenceToAxiom
+exception ReferenceToConstant
exception ReferenceToVariable
exception ReferenceToCurrentProof
exception ReferenceToInductiveDefinition
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
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 ;
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
+;;
*)
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
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;;
| 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 *)
| 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 ->
| 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
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
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
*)
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
exception CannotSubstInMeta;;
exception RelToHiddenHypothesis;;
+exception ReferenceToVariable;;
+exception ReferenceToConstant;;
+exception ReferenceToCurrentProof;;
+exception ReferenceToInductiveDefinition;;
let lift n =
let rec liftaux k =
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
| 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
| 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
| _ 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
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
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
| 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 =
* 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
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) ""))
| (_,_) -> 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)
) ;
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 =
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
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
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) ->
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) ->
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)
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 ->
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) ->
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
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 ->
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) ->
(* 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
| _ ->
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
)
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
)
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))
| 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 =
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
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
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
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
(*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
| 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
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
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
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
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
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
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
(*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
| 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))
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
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 &&
) 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
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))
)
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))
)
(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))
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)
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) ->
| 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 =
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
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)
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") ;
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
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
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
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)
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 *)
{ 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)
| 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
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
{ 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
;
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, []))
}
| 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
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 "<DELIFT2" ; flush stderr ;
- 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_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
| (he', metasenv'') -> 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''' =
p'::pl, metasenv'
) pl ([],metasenv'')
in
- C.MutCase (sp, cookingsno, i, outty', t', pl'),metasenv'''
+ C.MutCase (sp, i, outty', t', pl'),metasenv'''
| C.Fix (i, fl) ->
let len = List.length fl in
let liftedfl,metasenv' =
| _,_ -> 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
(* 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
(* 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 *)
"?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
+;;
(* 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
-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
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 =
+++ /dev/null
-(* $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.
- *
- *
- *)
+++ /dev/null
-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
+++ /dev/null
-(* 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 <sacerdot@cs.unibo.it> *)
-(* 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))
-;;
-
+++ /dev/null
-val from_file :
- ?alt:Csc_pxp_reader.resolver list ->
- ?system_encoding:Netconversion.encoding ->
- ?enc:Netconversion.encoding -> string -> Pxp_yacc.source
--- /dev/null
+(* 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 ()
+;;
--- /dev/null
+(* 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
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
+;;
(* 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
projects / helm.git / commitdiff