cicParser3.cmx: cic.cmx cicParser3.cmi
cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi
cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi
-cicParser.cmo: cicParser2.cmi cicParser3.cmi cicParser.cmi
-cicParser.cmx: cicParser2.cmx cicParser3.cmx cicParser.cmi
+cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi
+cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi
string * term * term (* name, type, body *)
and annterm =
- ARel of id * annotation option ref *
- int * string option (* DeBrujin index, binder *)
- | AVar of id * annotation option ref *
- UriManager.uri (* uri *)
- | AMeta of id * annotation option ref * int (* numeric id *)
- | ASort of id * annotation option ref * sort (* sort *)
- | AImplicit of id * annotation option ref (* *)
- | ACast of id * annotation option ref *
- annterm * annterm (* value, type *)
- | AProd of id * annotation option ref *
- name * annterm * annterm (* binder, source, target *)
- | ALambda of id * annotation option ref *
- name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * annotation option ref *
- name * annterm * annterm (* binder, term, target *)
- | AAppl of id * annotation option ref *
- annterm list (* arguments *)
- | AConst of id * annotation option ref *
- UriManager.uri * int (* uri, number of cookings*)
- | AAbst of id * annotation option ref *
- UriManager.uri (* uri *)
- | AMutInd of id * annotation option ref *
- UriManager.uri * int * int (* uri, cookingsno, typeno*)
- | AMutConstruct of id * annotation option ref *
- UriManager.uri * int * (* uri, cookingsno, *)
+ ARel of id * int * string (* DeBrujin index, binder *)
+ | AVar of id * UriManager.uri (* uri *)
+ | AMeta of id * int (* numeric id *)
+ | ASort of id * sort (* sort *)
+ | AImplicit of id (* *)
+ | ACast of id * annterm * annterm (* value, type *)
+ | AProd of id * name * annterm * annterm (* binder, source, target *)
+ | ALambda of id * name * annterm * annterm (* binder, source, target *)
+ | ALetIn of id * name * annterm * annterm (* binder, term, target *)
+ | AAppl of id * annterm list (* arguments *)
+ | AConst of id * UriManager.uri * int (* uri, number of cookings*)
+ | AAbst of id * UriManager.uri (* uri *)
+ | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*)
+ | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *)
int * int (* typeno, consno *)
(*CSC: serve cookingsno?*)
- | AMutCase of id * annotation option ref *
- UriManager.uri * int * (* ind. uri, cookingsno *)
+ | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *)
int * (* ind. typeno, *)
annterm * annterm * (* outtype, ind. term *)
annterm list (* patterns *)
- | AFix of id * annotation option ref *
- int * anninductiveFun list (* funno, functions *)
- | ACoFix of id * annotation option ref *
- int * anncoInductiveFun list (* funno, functions *)
+ | AFix of id * int * anninductiveFun list (* funno, functions *)
+ | ACoFix of id * int * anncoInductiveFun list (* funno, functions *)
and annobj =
- ADefinition of id * annotation option ref *
- string * (* id, *)
+ ADefinition of id * string * (* id, *)
annterm * annterm * (* value, type, *)
(int * UriManager.uri list) list exactness (* parameters *)
- | AAxiom of id * annotation option ref *
- string * annterm * (* id, type *)
+ | AAxiom of id * string * annterm * (* id, type *)
(int * UriManager.uri list) list (* parameters *)
- | AVariable of id * annotation option ref *
+ | AVariable of id *
string * annterm option * annterm (* name, body, type *)
- | ACurrentProof of id * annotation option ref *
+ | ACurrentProof of id *
string * (int * annterm) list * (* name, conjectures, *)
annterm * annterm (* value, type *)
| AInductiveDefinition of id *
- annotation option ref * anninductiveType list * (* inductive types , *)
+ anninductiveType list * (* inductive types , *)
(int * UriManager.uri list) list * int (* parameters,n ind. pars*)
and anninductiveType =
string * bool * annterm * (* typename, inductive, arity *)
;;
(* given the filename of an xml file of a cic object it returns its internal *)
-(* representation. process_annotations is true if the annotations do really *)
-(* matter *)
-let term_of_xml filename uri process_annotations =
+(* representation. *)
+let annobj_of_xml filename uri =
let module Y = Pxp_yacc in
try
let d =
(* sets the current base uri to resolve relative URIs *)
CicParser3.current_sp := tokens_of_uri uri ;
CicParser3.current_uri := uri ;
- CicParser3.process_annotations := process_annotations ;
- CicParser3.ids_to_targets :=
- if process_annotations then Some (Hashtbl.create 500) else None ;
let config = {Y.default_config with Y.warner = new warner} in
Y.parse_document_entity config
(*PXP (Y.ExtID (Pxp_types.System filename,
*) (PxpUriResolver.from_file filename)
CicParser3.domspec
in
- let ids_to_targets = !CicParser3.ids_to_targets in
- let res = (CicParser2.get_term d#root, ids_to_targets) in
- CicParser3.ids_to_targets := None ; (* let's help the GC *)
- res
+ CicParser2.get_term d#root
with
e ->
print_endline ("Filename: " ^ filename ^ "\nException: ") ;
print_endline (Pxp_types.string_of_exn e) ;
raise e
;;
+
+let obj_of_xml filename uri =
+ Deannotate.deannotate_obj (annobj_of_xml filename uri)
+;;
(******************************************************************************)
(* given the filename of an xml file of a cic object and it's uri, it returns *)
-(* its internal annotated representation. The boolean is set to true if the *)
-(* annotations do really matter *)
-val term_of_xml :
- string -> UriManager.uri -> bool ->
- Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t option
+(* its internal annotated representation. *)
+val annobj_of_xml : string -> UriManager.uri -> Cic.annobj
+
+(* given the filename of an xml file of a cic object and it's uri, it returns *)
+(* its internal logical representation. *)
+val obj_of_xml : string -> UriManager.uri -> Cic.obj
| _ -> raise (IllFormedXml 1)
;;
-let register_id id node =
- if !CicParser3.process_annotations then
- match !CicParser3.ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Object node)
-;;
-
(* Functions that, given the list of sons of a node of the cic dom (objects *)
(* level), retrieve the internal representation associated to the node. *)
(* Everytime a cic term subtree is found, it is translated to the internal *)
(v'#extension#to_cic_term, t'#extension#to_cic_term)
| _ -> raise (IllFormedXml 6)
and xid = string_of_attr (n#attribute "id") in
- let res = C.ADefinition (xid, ref None, id, value, typ, params) in
- register_id xid res ;
- res
+ C.ADefinition (xid, id, value, typ, params)
| D.T_element "Axiom" ->
let id = string_of_attr (n # attribute "name")
and params = uri_list_of_attr (n # attribute "params")
and typ =
(get_content (get_content n))#extension#to_cic_term
and xid = string_of_attr (n#attribute "id") in
- let res = C.AAxiom (xid, ref None, id, typ, params) in
- register_id xid res ;
- res
+ C.AAxiom (xid, id, typ, params)
| D.T_element "CurrentProof" ->
let name = string_of_attr (n#attribute "name")
and xid = string_of_attr (n#attribute "id") in
let sons = n#sub_nodes in
let (conjs, value, typ) = get_conjs_value_type sons in
- let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
- register_id xid res ;
- res
+ C.ACurrentProof (xid, name, conjs, value, typ)
| D.T_element "InductiveDefinition" ->
let sons = n#sub_nodes
and xid = string_of_attr (n#attribute "id") in
let inductiveTypes = get_inductive_types sons
and params = uri_list_of_attr (n#attribute "params")
and nparams = int_of_attr (n#attribute "noParams") in
- let res =
- C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
- in
- register_id xid res ;
- res
+ C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
and xid = string_of_attr (n#attribute "id")
(None, t'#extension#to_cic_term)
| _ -> raise (IllFormedXml 6)
in
- let res = C.AVariable (xid,ref None,name,body,typ) in
- register_id xid res ;
- res
+ C.AVariable (xid,name,body,typ)
| D.T_element _
| D.T_data
| _ ->
exception IllFormedXml of int;;
-(* The hashtable from the current identifiers to the object or the terms *)
-let ids_to_targets = ref None;;
-
(* The list of tokens of the current section path. *)
(* Used to resolve relative URIs *)
let current_sp = ref [];;
(* The uri of the object been parsed *)
let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
-(* True if annotation really matter *)
-let process_annotations = ref false;;
-
(* Utility functions to map a markup attribute to something useful *)
let cic_attr_of_xml_attr =
let binder_of_xml_attr =
function
- Pxp_types.Value s -> if !process_annotations then Some s else None
+ Pxp_types.Value s -> s
| _ -> raise (IllFormedXml 17)
;;
-let register_id id node =
- if !process_annotations then
- match !ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Term node)
-;;
-
(* the "interface" of the class linked to each node of the dom tree *)
class virtual cic_term =
| _ -> raise (IllFormedXml 13)
) sons
in
- let res = Cic.AFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.AFix (id, nofun, functions)
end
;;
| _ -> raise (IllFormedXml 15)
) sons
in
- let res = Cic.ACoFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.ACoFix (id, nofun, functions)
end
;;
method to_cic_term =
let n = self#node in
let id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AImplicit (id, ref None) in
- register_id id res ;
- res
+ Cic.AImplicit id
end
;;
let value = int_of_xml_attr (n#attribute "value")
and binder = binder_of_xml_attr (n#attribute "binder")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ARel (id,ref None,value,binder) in
- register_id id res ;
- res
+ Cic.ARel (id,value,binder)
end
;;
let n = self#node in
let value = int_of_xml_attr (n#attribute "no")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AMeta (id,ref None,value) in
- register_id id res ;
- res
+ Cic.AMeta (id,value)
end
;;
in
aux (List.length !current_sp - n,!current_sp)
in
- let res =
- Cic.AVar
- (xid,ref None,
- (UriManager.uri_of_string
- ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
- )
- in
- register_id id res ;
- res
+ Cic.AVar
+ (xid,
+ (UriManager.uri_of_string
+ ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
+ )
| _ -> raise (IllFormedXml 18)
end
;;
and id = string_of_xml_attr (n#attribute "id") in
if List.length children < 2 then raise (IllFormedXml 8)
else
- let res =
- Cic.AAppl
- (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
- in
- register_id id res ;
- res
+ Cic.AAppl
+ (id,List.map (fun x -> x#extension#to_cic_term) children)
end
;;
ty#node_type = Pxp_document.T_element "type" ->
let term = te#extension#to_cic_term
and typ = ty#extension#to_cic_term in
- let res = Cic.ACast (id,ref None,term,typ) in
- register_id id res ;
- res
+ Cic.ACast (id,term,typ)
| _ -> raise (IllFormedXml 9)
end
;;
let n = self#node in
let sort = cic_sort_of_xml_attr (n#attribute "value")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ASort (id,ref None,sort) in
- register_id id res ;
- res
+ Cic.ASort (id,sort)
end
;;
let n = self#node in
let value = uri_of_xml_attr (n#attribute "uri")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AAbst (id,ref None,value) in
- register_id id res ;
- res
+ Cic.AAbst (id,value)
end
;;
let n = self#node in
let value = uri_of_xml_attr (n#attribute "uri")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
- in
- register_id id res ;
- res
+ Cic.AConst (id,value, U.relative_depth !current_uri value 0)
end
;;
let name = uri_of_xml_attr (n#attribute "uri")
and noType = int_of_xml_attr (n#attribute "noType")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutInd
- (id,ref None,name, U.relative_depth !current_uri name 0, noType)
- in
- register_id id res ;
- res
+ Cic.AMutInd
+ (id,name, U.relative_depth !current_uri name 0, noType)
end
;;
and noType = int_of_xml_attr (n#attribute "noType")
and noConstr = int_of_xml_attr (n#attribute "noConstr")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutConstruct
- (id, ref None, name, U.relative_depth !current_uri name 0,
- noType, noConstr)
- in
- register_id id res ;
- res
+ Cic.AMutConstruct
+ (id, name, U.relative_depth !current_uri name 0,
+ noType, noConstr)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.AProd (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.AProd (id,name,source,target)
| _ -> raise (IllFormedXml 10)
end
;;
and inductiveTerm = te#extension#to_cic_term
and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
in
- let res =
- Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
- typeno,inductiveType,inductiveTerm,lpattern)
- in
- register_id id res ;
- res
+ Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
+ typeno,inductiveType,inductiveTerm,lpattern)
| _ -> raise (IllFormedXml 11)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.ALambda (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.ALambda (id,name,source,target)
| _ -> raise (IllFormedXml 12)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.ALetIn (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.ALetIn (id,name,source,target)
| _ -> raise (IllFormedXml 12)
end
;;
exception IllFormedXml of int
-val ids_to_targets : (Cic.id, Cic.anntarget) Hashtbl.t option ref
val current_sp : string list ref
val current_uri : UriManager.uri ref
-val process_annotations : bool ref
(* the "interface" of the class linked to each node of the dom tree *)
class virtual cic_term :
let rec deannotate_term =
let module C = Cic in
function
- C.ARel (_,_,n,_) -> C.Rel n
- | C.AVar (_,_,uri) -> C.Var uri
- | C.AMeta (_,_,n) -> C.Meta n
- | C.ASort (_,_,s) -> C.Sort s
+ C.ARel (_,n,_) -> C.Rel n
+ | C.AVar (_,uri) -> C.Var uri
+ | C.AMeta (_,n) -> C.Meta n
+ | C.ASort (_,s) -> C.Sort s
| C.AImplicit _ -> C.Implicit
- | C.ACast (_,_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
- | C.AProd (_,_,name,so,ta) ->
+ | C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
+ | C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)
- | C.ALambda (_,_,name,so,ta) ->
+ | C.ALambda (_,name,so,ta) ->
C.Lambda (name, deannotate_term so, deannotate_term ta)
- | C.ALetIn (_,_,name,so,ta) ->
+ | C.ALetIn (_,name,so,ta) ->
C.LetIn (name, deannotate_term so, deannotate_term ta)
- | C.AAppl (_,_,l) -> C.Appl (List.map deannotate_term l)
- | C.AConst (_,_,uri, cookingsno) -> C.Const (uri, cookingsno)
- | C.AAbst (_,_,uri) -> C.Abst uri
- | C.AMutInd (_,_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
- | C.AMutConstruct (_,_,uri,cookingsno,i,j) ->
+ | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
+ | C.AConst (_,uri, cookingsno) -> C.Const (uri, cookingsno)
+ | C.AAbst (_,uri) -> C.Abst uri
+ | C.AMutInd (_,uri,cookingsno,i) -> C.MutInd (uri,cookingsno,i)
+ | C.AMutConstruct (_,uri,cookingsno,i,j) ->
C.MutConstruct (uri,cookingsno,i,j)
- | C.AMutCase (_,_,uri,cookingsno,i,outtype,te,pl) ->
+ | C.AMutCase (_,uri,cookingsno,i,outtype,te,pl) ->
C.MutCase (uri,cookingsno,i,deannotate_term outtype,
deannotate_term te, List.map deannotate_term pl)
- | C.AFix (_,_,funno,ifl) ->
+ | C.AFix (_,funno,ifl) ->
C.Fix (funno, List.map deannotate_inductiveFun ifl)
- | C.ACoFix (_,_,funno,ifl) ->
+ | C.ACoFix (_,funno,ifl) ->
C.CoFix (funno, List.map deannotate_coinductiveFun ifl)
and deannotate_inductiveFun (name,index,ty,bo) =
let deannotate_obj =
let module C = Cic in
function
- C.ADefinition (_, _, id, bo, ty, params) ->
+ C.ADefinition (_, id, bo, ty, params) ->
(match params with
C.Possible params ->
if !expect_possible_parameters then
| C.Actual params ->
C.Definition (id, deannotate_term bo, deannotate_term ty, params)
)
- | C.AAxiom (_, _, id, ty, params) ->
+ | C.AAxiom (_, id, ty, params) ->
C.Axiom (id, deannotate_term ty, params)
- | C.AVariable (_, _, name, bo, ty) ->
+ | C.AVariable (_, name, bo, ty) ->
C.Variable (name,
(match bo with None -> None | Some bo -> Some (deannotate_term bo)),
deannotate_term ty)
- | C.ACurrentProof (_, _, name, conjs, bo, ty) ->
+ | C.ACurrentProof (_, name, conjs, bo, ty) ->
C.CurrentProof (
name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
deannotate_term bo, deannotate_term ty
)
- | C.AInductiveDefinition (_, _, tys, params, parno) ->
+ | C.AInductiveDefinition (_, tys, params, parno) ->
C.InductiveDefinition ( List.map deannotate_inductiveType tys,
params, parno)
;;
-cicAnnotation2Xml.cmo: cicAnnotation2Xml.cmi
-cicAnnotation2Xml.cmx: cicAnnotation2Xml.cmi
-cicAnnotationHinter.cmo: cicAnnotationHinter.cmi
-cicAnnotationHinter.cmx: cicAnnotationHinter.cmi
+cicXPath.cmo: cicXPath.cmi
+cicXPath.cmx: cicXPath.cmi
+cicAnnotation2Xml.cmo: cicXPath.cmi cicAnnotation2Xml.cmi
+cicAnnotation2Xml.cmx: cicXPath.cmx cicAnnotation2Xml.cmi
cicAnnotationParser2.cmo: cicAnnotationParser2.cmi
cicAnnotationParser2.cmx: cicAnnotationParser2.cmi
cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi
cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi
-cicXPath.cmo: cicXPath.cmi
-cicXPath.cmx: cicXPath.cmi
REQUIRES = helm-cic helm-xml
PREDICATES =
-INTERFACE_FILES = cicAnnotation2Xml.mli cicAnnotationParser2.mli \
- cicAnnotationParser.mli cicXPath.mli
+INTERFACE_FILES = cicXPath.mli cicAnnotation2Xml.mli cicAnnotationParser2.mli \
+ cicAnnotationParser.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";;
+let get_ann ids_to_annotations =
+ CicXPath.get_annotation ids_to_annotations
+;;
+
+let print_ann i2a id =
+ let module X = Xml in
+ let ann = get_ann i2a id in
+ match ann with
+ None -> [<>]
+ | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
+;;
+
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term =
+let print_term i2a =
let rec aux =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
function
- C.ARel (id,ann,_,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.AVar (id,ann,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.AMeta (id,ann,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.ASort (id,ann,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
+ C.ARel (id,_,_) -> print_ann i2a id
+ | C.AVar (id,_) -> print_ann i2a id
+ | C.AMeta (id,_) -> print_ann i2a id
+ | C.ASort (id,_) -> print_ann i2a id
| C.AImplicit _ -> raise NotImplemented
- | C.AProd (id,ann,_,s,t) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
- aux s ;
- aux t
- >]
- | C.ACast (id,ann,v,t) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
- aux v ;
- aux t
- >]
- | C.ALambda (id,ann,_,s,t) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
- aux s ;
- aux t
- >]
- | C.ALetIn (id,ann,_,s,t) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
- aux s ;
- aux t
- >]
- | C.AAppl (id,ann,li) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
+ | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+ | C.ACast (id,v,t) -> [< print_ann i2a id ; aux v ; aux t >]
+ | C.ALambda (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+ | C.ALetIn (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
+ | C.AAppl (id,li) ->
+ [< print_ann i2a id ;
List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
>]
- | C.AConst (id,ann,_,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.AAbst (id,ann,_) -> raise NotImplemented
- | C.AMutInd (id,ann,_,_,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.AMutConstruct (id,ann,_,_,_,_) ->
- (match !ann with
- None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- )
- | C.AMutCase (id,ann,_,_,_,ty,te,patterns) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
+ | C.AConst (id,_,_) -> print_ann i2a id
+ | C.AAbst (id,_) -> raise NotImplemented
+ | C.AMutInd (id,_,_,_) -> print_ann i2a id
+ | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
+ | C.AMutCase (id,_,_,_,ty,te,patterns) ->
+ [< print_ann i2a id ;
aux ty ;
aux te ;
List.fold_right
(fun x i -> [< aux x ; i>])
patterns [<>]
>]
- | C.AFix (id, ann, _, funs) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
+ | C.AFix (id,_,funs) ->
+ [< print_ann i2a id ;
List.fold_right
(fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
>]
- | C.ACoFix (id, ann,no,funs) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
- ) ;
+ | C.ACoFix (id,no,funs) ->
+ [< print_ann i2a id ;
List.fold_right
(fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
>]
aux
;;
-let print_mutual_inductive_type (_,_,arity,constructors) =
- [< print_term arity ;
+let print_mutual_inductive_type i2a (_,_,arity,constructors) =
+ [< print_term i2a arity ;
List.fold_right
- (fun (name,ty,_) i -> [< print_term ty ; i >]) constructors [<>]
+ (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>]
>]
;;
-let pp_annotation obj curi =
+let pp_annotation obj i2a curi =
let module C = Cic in
let module X = Xml in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
begin
match obj with
- C.ADefinition (xid, ann, _, te, ty, _) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
- ) ;
- print_term te ;
- print_term ty
- >]
- | C.AAxiom (xid, ann, _, ty, _) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
- ) ;
- print_term ty
- >]
- | C.AVariable (xid, ann, _, bo, ty) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
- ) ;
+ C.ADefinition (xid, _, te, ty, _) ->
+ [< print_ann i2a xid ; print_term i2a te ; print_term i2a ty >]
+ | C.AAxiom (xid, _, ty, _) -> [< print_ann i2a xid ; print_term i2a ty >]
+ | C.AVariable (xid, _, bo, ty) ->
+ [< print_ann i2a xid ;
(match bo with
None -> [<>]
- | Some bo -> print_term bo
+ | Some bo -> print_term i2a bo
) ;
- print_term ty
+ print_term i2a ty
>]
- | C.ACurrentProof (xid, ann, _, conjs, bo, ty) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
- ) ;
+ | C.ACurrentProof (xid, _, conjs, bo, ty) ->
+ [< print_ann i2a xid ;
List.fold_right
- (fun (_,t) i -> [< print_term t ; i >])
+ (fun (_,t) i -> [< print_term i2a t ; i >])
conjs [<>] ;
- print_term bo ;
- print_term ty
+ print_term i2a bo ;
+ print_term i2a ty
>]
- | C.AInductiveDefinition (xid, ann, tys, params, paramsno) ->
- [< (match !ann with
- None -> [<>]
- | Some ann ->
- X.xml_nempty "Annotation" ["of", xid] (X.xml_cdata ann)
- ) ;
+ | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+ [< print_ann i2a xid ;
List.fold_right
- (fun x i -> [< print_mutual_inductive_type x ; i >])
+ (fun x i -> [< print_mutual_inductive_type i2a x ; i >])
tys [< >]
>]
end
(* *)
(******************************************************************************)
-val pp_annotation : Cic.annobj -> UriManager.uri -> Xml.token Stream.t
+val pp_annotation :
+ Cic.annobj -> (Cic.id, string) Hashtbl.t -> UriManager.uri ->
+ Xml.token Stream.t
exception EmptyUri;;
-let annotate filename ids_to_targets =
+let get_annotations filename =
let module Y = Pxp_yacc in
try
let d =
Y.default_spec
in
- CicAnnotationParser2.annotate ids_to_targets d#root
+ CicAnnotationParser2.get_annotations d#root
with
e ->
print_endline (Pxp_types.string_of_exn e) ;
(* *)
(******************************************************************************)
-val annotate : string -> (string, Cic.anntarget) Hashtbl.t -> unit
+val get_annotations : string -> (Cic.id, string) Hashtbl.t
| _ -> raise DontKnowWhatToDo
;;
-let get_annotation n =
+let get_annotation_from_node n =
String.concat "" (List.map string_of_annotations (n#sub_nodes))
;;
-let annotate_object ann obj =
- let module C = Cic in
- let rann =
- match obj with
- C.ADefinition (_, rann, _, _, _, _) -> rann
- | C.AAxiom (_, rann, _, _, _) -> rann
- | C.AVariable (_, rann, _, _, _) -> rann
- | C.ACurrentProof (_, rann, _, _, _, _) -> rann
- | C.AInductiveDefinition (_, rann, _, _, _) -> rann
- in
- rann := Some ann
-;;
+exception MoreThanOneAnnotationFor of Cic.id;;
-let annotate_term ann term =
- let module C = Cic in
- let rann =
- match term with
- C.ARel (_, rann, _, _) -> rann
- | C.AVar (_, rann, _) -> rann
- | C.AMeta (_, rann, _) -> rann
- | C.ASort (_, rann, _) -> rann
- | C.AImplicit (_, rann) -> rann
- | C.ACast (_, rann, _, _) -> rann
- | C.AProd (_, rann, _, _, _) -> rann
- | C.ALambda (_, rann, _, _, _) -> rann
- | C.ALetIn (_, rann, _, _, _) -> rann
- | C.AAppl (_, rann, _) -> rann
- | C.AConst (_, rann, _, _) -> rann
- | C.AAbst (_, rann, _) -> rann
- | C.AMutInd (_, rann, _, _, _) -> rann
- | C.AMutConstruct (_, rann, _, _, _, _) -> rann
- | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
- | C.AFix (_, rann, _, _) -> rann
- | C.ACoFix (_, rann, _, _) -> rann
- in
- rann := Some ann
+let set_annotation ids_to_annotations id ann =
+ try
+ ignore (Hashtbl.find ids_to_annotations id) ;
+ raise (MoreThanOneAnnotationFor id)
+ with
+ Not_found -> Hashtbl.add ids_to_annotations id ann
;;
-let annotate ids_to_targets n =
+let get_annotations n =
let module D = Pxp_document in
let module C = Cic in
- let annotate_elem n =
- let ntype = n # node_type in
- match ntype with
- D.T_element "Annotation" ->
- let of_uri = string_of_attr (n # attribute "of") in
- begin
- try
- match Hashtbl.find ids_to_targets of_uri with
- C.Object o -> annotate_object (get_annotation n) o
- | C.Term t -> annotate_term (get_annotation n) t
- with
- Not_found -> assert false
- end
- | D.T_element _ | D.T_data ->
- raise (IllFormedXml 1)
- | _ -> raise DontKnowWhatToDo
- in
- match n # node_type with
- D.T_element "Annotations" ->
- List.iter annotate_elem (n # sub_nodes)
- | _ -> raise (IllFormedXml 2)
+ let ids_to_annotations = Hashtbl.create 503 in
+ let annotate_elem n =
+ let ntype = n # node_type in
+ match ntype with
+ D.T_element "Annotation" ->
+ let of_uri = string_of_attr (n # attribute "of") in
+ set_annotation ids_to_annotations of_uri (get_annotation_from_node n)
+ | D.T_element _ | D.T_data ->
+ raise (IllFormedXml 1)
+ | _ -> raise DontKnowWhatToDo
+ in
+ match n # node_type with
+ D.T_element "Annotations" ->
+ List.iter annotate_elem (n # sub_nodes) ;
+ ids_to_annotations
+ | _ -> raise (IllFormedXml 2)
;;
(******************************************************************************)
exception IllFormedXml of int
-val annotate :
- (string, Cic.anntarget) Hashtbl.t ->
+val get_annotations :
< node_type : Pxp_document.node_type;
sub_nodes : < attribute : string -> Pxp_types.att_value;
node_type : Pxp_document.node_type;
.. >
list;
.. > ->
- unit
+ (Cic.id, string) Hashtbl.t
(* *)
(******************************************************************************)
-let get_annotation_from_term annterm =
- let module C = Cic in
- match annterm with
- C.ARel (_,ann,_,_) -> ann
- | C.AVar (_,ann,_) -> ann
- | C.AMeta (_,ann,_) -> ann
- | C.ASort (_,ann,_) -> ann
- | C.AImplicit (_,ann) -> ann
- | C.ACast (_,ann,_,_) -> ann
- | C.AProd (_,ann,_,_,_) -> ann
- | C.ALambda (_,ann,_,_,_) -> ann
- | C.ALetIn (_,ann,_,_,_) -> ann
- | C.AAppl (_,ann,_) -> ann
- | C.AConst (_,ann,_,_) -> ann
- | C.AAbst (_,ann,_) -> ann
- | C.AMutInd (_,ann,_,_,_) -> ann
- | C.AMutConstruct (_,ann,_,_,_,_)-> ann
- | C.AMutCase (_,ann,_,_,_,_,_,_) -> ann
- | C.AFix (_,ann,_,_) -> ann
- | C.ACoFix (_,ann,_,_) -> ann
-;;
-
-let get_annotation_from_obj annobj =
- let module C = Cic in
- match annobj with
- C.ADefinition (_,ann,_,_,_,_) -> ann
- | C.AAxiom (_,ann,_,_,_) -> ann
- | C.AVariable (_,ann,_,_,_) -> ann
- | C.ACurrentProof (_,ann,_,_,_,_) -> ann
- | C.AInductiveDefinition (_,ann,_,_,_) -> ann
+let get_annotation ids_to_annotations xpath =
+ try
+ Some (Hashtbl.find ids_to_annotations xpath)
+ with
+ Not_found -> None
;;
-exception IdUnknown of string;;
+exception MoreThanOneTargetFor of Cic.id;;
-let get_annotation (annobj,ids_to_targets) xpath =
- try
- match Hashtbl.find ids_to_targets xpath with
- Cic.Object annobj -> get_annotation_from_obj annobj
- | Cic.Term annterm -> get_annotation_from_term annterm
- with
- Not_found -> raise (IdUnknown xpath)
+let get_ids_to_targets annobj =
+ let module C = Cic in
+ let ids_to_targets = Hashtbl.create 503 in
+ let set_target id target =
+ try
+ ignore (Hashtbl.find ids_to_targets id) ;
+ raise (MoreThanOneTargetFor id)
+ with
+ Not_found -> Hashtbl.add ids_to_targets id target
+ in
+ let rec add_target_term t =
+ match t with
+ C.ARel (id,_,_)
+ | C.AVar (id,_)
+ | C.AMeta (id,_)
+ | C.ASort (id,_)
+ | C.AImplicit id ->
+ set_target id (C.Term t)
+ | C.ACast (id,va,ty) ->
+ set_target id (C.Term t) ;
+ add_target_term va ;
+ add_target_term ty
+ | C.AProd (id,_,so,ta)
+ | C.ALambda (id,_,so,ta)
+ | C.ALetIn (id,_,so,ta) ->
+ set_target id (C.Term t) ;
+ add_target_term so ;
+ add_target_term ta
+ | C.AAppl (id,l) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term l
+ | C.AConst (id,_,_)
+ | C.AAbst (id,_)
+ | C.AMutInd (id,_,_,_)
+ | C.AMutConstruct (id,_,_,_,_) ->
+ set_target id (C.Term t)
+ | C.AMutCase (id,_,_,_,ot,it,pl) ->
+ set_target id (C.Term t) ;
+ List.iter add_target_term (ot::it::pl)
+ | C.AFix (id,_,ifl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) ifl
+ | C.ACoFix (id,_,cfl) ->
+ set_target id (C.Term t) ;
+ List.iter
+ (function (_,ty,bo) ->
+ add_target_term ty ;
+ add_target_term bo
+ ) cfl
+ in
+ let add_target_obj annobj =
+ match annobj with
+ C.ADefinition (id,_,bo,ty,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.AAxiom (id,_,ty,_) ->
+ set_target id (C.Object annobj) ;
+ add_target_term ty
+ | C.AVariable (id,_,None,ty) ->
+ set_target id (C.Object annobj) ;
+ add_target_term ty
+ | C.AVariable (id,_,Some bo,ty) ->
+ set_target id (C.Object annobj) ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.ACurrentProof (id,_,cl,bo,ty) ->
+ set_target id (C.Object annobj) ;
+ List.iter (function (_,t) -> add_target_term t) cl ;
+ add_target_term bo ;
+ add_target_term ty
+ | C.AInductiveDefinition (id,itl,_,_) ->
+ set_target id (C.Object annobj) ;
+ List.iter
+ (function (_,_,arity,cl) ->
+ add_target_term arity ;
+ List.iter (function (_,ty,_) -> add_target_term ty) cl
+ ) itl
+ in
+ add_target_obj annobj ;
+ ids_to_targets
;;
(******************************************************************************)
val get_annotation :
- 'a * (string, Cic.anntarget) Hashtbl.t -> string -> string option ref
+ (Cic.id, string) Hashtbl.t -> Cic.id -> string option
+
+val get_ids_to_targets : Cic.annobj -> (Cic.id, Cic.anntarget) Hashtbl.t
let module G = Getter in
let module U = UriManager in
let cicfilename = G.getxml (U.cicuri_of_uri uri) in
- match CicParser.term_of_xml cicfilename uri true with
- (_, None) -> assert false
- | (annobj, Some ids_to_targets) ->
- if U.uri_is_annuri uri then
- begin
- let annfilename = G.getxml (U.annuri_of_uri uri) in
- CicAnnotationParser.annotate annfilename ids_to_targets
- end ;
- (annobj, ids_to_targets)
+ let annobj = CicParser.annobj_of_xml cicfilename uri in
+ annobj,
+ if U.uri_is_annuri uri then
+ begin
+ let annfilename = G.getxml (U.annuri_of_uri uri) in
+ Some (CicAnnotationParser.get_annotations annfilename)
+ end
+ else
+ None
;;
(******************************************************************************)
val get_annobj :
- UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t
+ UriManager.uri -> Cic.annobj * (Cic.id, string) Hashtbl.t option
let module G = Getter in
let module U = UriManager in
let cicfilename = G.getxml (U.cicuri_of_uri uri) in
- match CicParser.term_of_xml cicfilename uri false with
- (_, Some _) -> assert false
- | (annobj, None) -> annobj
+ CicParser.annobj_of_xml cicfilename uri
;;
let get_obj uri =
- Deannotate.deannotate_obj (get_annobj uri)
+ let module G = Getter in
+ let module U = UriManager in
+ let cicfilename = G.getxml (U.cicuri_of_uri uri) in
+ CicParser.obj_of_xml cicfilename uri
;;
C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype)
| _ -> raise (WrongUriToVariable (U.string_of_uri var))
in
- cookrec (add_binder (C.Name varname) varbody vartype
- (cook curi cookingsno var ty)) tl
+ let cooked_once =
+ add_binder (C.Name varname) varbody vartype
+ (match varbody with
+ Some _ -> ty
+ | None -> cook curi cookingsno var ty
+ )
+ in
+ cookrec cooked_once tl
| _ -> ty
in
cookrec ty vars
with
Not_found ->
let filename = Getter.getxml uri in
- let (annobj,_) = CicParser.term_of_xml filename uri false in
- let obj = Deannotate.deannotate_obj annobj in
- let output = Unchecked obj in
- HashTable.add hashtable (uri,0) output ;
- output
-;;
-
-(* DANGEROUS!!! *)
-(* USEFUL ONLY DURING THE FIXING OF THE FILES *)
-(* change_obj uri (Some newobj) *)
-(* maps uri to newobj in cache. *)
-(* change_obj uri None *)
-(* maps uri to a freeze dummy-object. *)
-let change_obj uri newobj =
- let newobj =
- match newobj with
- Some newobj' -> Unchecked newobj'
- | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit))
- in
- HashTable.remove hashtable (uri,0) ;
- HashTable.add hashtable (uri,0) newobj
+ let obj = CicParser.obj_of_xml filename uri in
+ let output = Unchecked obj in
+ HashTable.add hashtable (uri,0) output ;
+ output
;;
let is_annotation_uri uri =
Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0
;;
-(* returns both the annotated and deannotated uncooked forms (plus the *)
-(* map from ids to annotation targets) *)
-let get_annobj_and_type_checking_info uri =
- let filename = Getter.getxml uri in
- match CicParser.term_of_xml filename uri true with
- (_, None) -> raise Impossible
- | (annobj, Some ids_to_targets) ->
- (* If uri is the uri of an annotation, let's use the annotation file *)
- if is_annotation_uri uri then
-(* CSC: la roba annotata non dovrebbe piu' servire
- AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ;
-*) assert false ;
- try
- (annobj, ids_to_targets, HashTable.find hashtable (uri,0))
- with
- Not_found ->
- let obj = Deannotate.deannotate_obj annobj in
- let output = Unchecked obj in
- HashTable.add hashtable (uri,0) output ;
- (annobj, ids_to_targets, output)
-;;
-
-
(* get_obj uri *)
(* returns the cic object whose uri is uri. If the term is not just in cache, *)
(* then it is parsed via CicParser.term_of_xml from the file whose name is *)
| Cooked obj -> obj
;;
-(* get_annobj uri *)
-(* returns the cic object whose uri is uri either in annotated and *)
-(* deannotated form. The term is put into the cache if it's not there yet. *)
-let get_annobj uri =
- let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in
- let deannobj =
- match deann with
- Unchecked obj -> obj
- | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri))
- | Cooked obj -> obj
- in
- (ann, ids_to_targets, deannobj)
-;;
-
(*CSC Commento falso *)
(* get_obj uri *)
(* returns the cooked cic object whose uri is uri. The term must be present *)
(* the result of Getter.get uri *)
val get_obj : UriManager.uri -> Cic.obj
-(* get_annobj uri *)
-(* returns the cic object whose uri is uri either in annotated and in *)
-(* deannotated form. It returns also the map from ids to annotation targets. *)
-(* The term is put in cache if it's not there yet. *)
-(* The functions raise CircularDependency if asked to retrieve a Frozen object*)
-val get_annobj :
- UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t * Cic.obj
-
-(* DANGEROUS!!! *)
-(* USEFUL ONLY DURING THE FIXING OF THE FILES *)
-(* change_obj uri (Some newobj) *)
-(* maps uri to newobj in cache. *)
-(* change_obj uri None *)
-(* maps uri to a freeze dummy-object. *)
-val change_obj : UriManager.uri -> Cic.obj option -> unit
-
type type_checked_obj =
CheckedObj of Cic.obj (* cooked obj *)
| UncheckedObj of Cic.obj (* uncooked obj *)
(******************************************************************************)
exception CicPpInternalError;;
+exception NotEnoughElements;;
(* Utility functions *)
| Cic.Anonimous -> "_"
;;
-(* get_nth l n returns the nth element of the list l if it exists or raise *)
-(* a CicPpInternalError if l has less than n elements or n < 1 *)
+(* get_nth l n returns the nth element of the list l if it exists or *)
+(* raises NotEnoughElements if l has less than n elements *)
let rec get_nth l n =
match (n,l) with
(1, he::_) -> he
| (n, he::tail) when n > 1 -> get_nth tail (n-1)
- | (_,_) -> raise CicPpInternalError
+ | (_,_) -> raise NotEnoughElements
;;
(* pp t l *)
let module C = Cic in
match t with
C.Rel n ->
- (match get_nth l n with
- C.Name s -> s
- | _ -> raise CicPpInternalError
- )
+ begin
+ try
+ (match get_nth l n with
+ C.Name s -> s
+ | _ -> raise CicPpInternalError
+ )
+ with
+ NotEnoughElements -> string_of_int (List.length l - n)
+ end
| C.Var uri -> UriManager.name_of_uri uri
| C.Meta n -> "?" ^ (string_of_int n)
| C.Sort s ->
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None,
- C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
- C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
- C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
- C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
- C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
- C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
- C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
- C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
- C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
- t
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )) ^ "\n" ^ i
+ CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
in
if !fdebug = 0 then
begin
let module S = CicSubstitution in
function
C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
- | C.Var _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Var uri as t ->
+ (match CicEnvironment.get_cooked_obj uri 0 with
+ C.Definition _ -> raise ReferenceToDefinition
+ | C.Axiom _ -> raise ReferenceToAxiom
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
+ | C.Variable (_,Some body,_) -> whdaux l body
+ )
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
| C.Implicit as t -> t
(match CicEnvironment.get_cooked_obj uri cookingsno with
C.Definition (_,body,_,_) -> whdaux l body
| C.Axiom _ -> if l = [] then t else C.Appl (t::l)
- (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *)
- | C.Variable _ -> if l = [] then t else C.Appl (t::l)
+ | C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,body,_) -> whdaux l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
| (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
| (C.Implicit, _) | (_, C.Implicit) ->
raise (Impossible 3) (* we don't trust our whd ;-) *)
- | (_,_) -> false
+ | (_,_) ->
+ debug t1' [t2'] "NOT-CONVERTIBLE" ;
+ false
end
in
aux t1 t2
let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None,
- C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
- C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
- C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
- C.Prod (C.Name "-12", C.Const (U.uri_of_string "cic:/dummy-12",0),
- C.Prod (C.Name "-11", C.Const (U.uri_of_string "cic:/dummy-11",0),
- C.Prod (C.Name "-10", C.Const (U.uri_of_string "cic:/dummy-10",0),
- C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
- C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
- C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
- C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
- C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
- C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
- C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
- C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
- C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
- t
- )
- )
- )
- )
- )
- )
- )
- )
- )))))))
- )) ^ "\n" ^ i
+ CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
in
if !fdebug = 0 then
raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) ""))
projects / helm.git / commitdiff