| "REL" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["binder", binder; "id", id; "idref", idref; "value", value]
| ["binder", binder; "id", id; "idref", idref; "sort", _;
"value", value] ->
Cic.ARel (id, idref, int_of_string value, binder)
| "VAR" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "uri", uri]
| ["id", id; "sort", _; "uri", uri] ->
Cic.AVar (id, uri_of_string uri, [])
| _ -> attribute_error ()))
| "CONST" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "uri", uri]
| ["id", id; "sort", _; "uri", uri] ->
Cic.AConst (id, uri_of_string uri, [])
| _ -> attribute_error ()))
let args = pop_cics ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id ]
| ["id", id; "sort", _] -> Cic.AAppl (id, args)
| _ -> attribute_error ()))
| "decl" ->
let source = pop_cic ctxt in
push ctxt
(match pop_tag_attrs ctxt with
+ | ["binder", binder; "id", id ]
| ["binder", binder; "id", id; "type", _] ->
Decl (id, Cic.Name binder, source)
+ | ["id", id]
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
let source = pop_cic ctxt in
push ctxt
(match pop_tag_attrs ctxt with
+ | ["binder", binder; "id", id]
| ["binder", binder; "id", id; "sort", _] ->
Def (id, Cic.Name binder, source)
+ | ["id", id]
| ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "arity" (* transparent elements (i.e. which contain a CIC) *)
in
let term = add_decl target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["type", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
in
let term = add_decl target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["sort", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
in
let term = add_def target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["sort", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
let term = pop_cic ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ ["id", id]
| ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
| _ -> attribute_error ()));
| "IMPLICIT" ->
let meta_substs = pop_meta_substs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "no", no]
| ["id", id; "no", no; "sort", _] ->
Cic.AMeta (id, int_of_string no, meta_substs)
| _ -> attribute_error ()));
| "MUTCONSTRUCT" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri]
| ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
"uri", uri] ->
Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
let fix_funs = pop_fix_funs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noFun", noFun]
| ["id", id; "noFun", noFun; "sort", _] ->
Cic.AFix (id, int_of_string noFun, fix_funs)
| _ -> attribute_error ()))
let cofix_funs = pop_cofix_funs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noFun", noFun]
| ["id", id; "noFun", noFun; "sort", _] ->
Cic.ACoFix (id, int_of_string noFun, cofix_funs)
| _ -> attribute_error ()))
| patternsType :: inductiveTerm :: patterns ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noType", noType; "uriType", uriType]
| ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
patternsType, inductiveTerm, patterns)
aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
ids_to_conjectures,ids_to_hypotheses
;;
+
+let plain_acic_term_of_cic_term =
+ let module C = Cic in
+ let mk_fresh_id =
+ let id = ref 0 in
+ function () -> incr id; "i" ^ string_of_int !id in
+ let rec aux context t =
+ let fresh_id = mk_fresh_id () in
+ match t with
+ C.Rel n ->
+ let idref,id =
+ match get_nth context n with
+ idref,(Some (C.Name s,_)) -> idref,s
+ | idref,_ -> idref,"__" ^ string_of_int n
+ in
+ C.ARel (fresh_id, idref, n, id)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AVar (fresh_id,uri,exp_named_subst')
+ | C.Implicit _
+ | C.Meta _ -> assert false
+ | C.Sort s -> C.ASort (fresh_id, s)
+ | C.Cast (v,t) ->
+ C.ACast (fresh_id, aux context v, aux context t)
+ | C.Prod (n,s,t) ->
+ C.AProd
+ (fresh_id, n, aux context s,
+ aux ((fresh_id, Some (n, C.Decl s))::context) t)
+ | C.Lambda (n,s,t) ->
+ C.ALambda
+ (fresh_id,n, aux context s,
+ aux ((fresh_id, Some (n, C.Decl s))::context) t)
+ | C.LetIn (n,s,t) ->
+ C.ALetIn
+ (fresh_id, n, aux context s,
+ aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+ | C.Appl l ->
+ C.AAppl (fresh_id, List.map (aux context) l)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AConst (fresh_id, uri, exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AMutInd (fresh_id, uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux context t)) exp_named_subst
+ in
+ C.AMutConstruct (fresh_id, uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri, tyno, outty, term, patterns) ->
+ C.AMutCase (fresh_id, uri, tyno, aux context outty,
+ aux context term, List.map (aux context) patterns)
+ | C.Fix (funno, funs) ->
+ let tys =
+ List.map
+ (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+ in
+ C.AFix (fresh_id, funno,
+ List.map2
+ (fun (id,_) (name, indidx, ty, bo) ->
+ (id, name, indidx, aux context ty, aux (tys@context) bo)
+ ) tys funs
+ )
+ | C.CoFix (funno, funs) ->
+ let tys =
+ List.map (fun (name,ty,_) ->
+ mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+ in
+ C.ACoFix (fresh_id, funno,
+ List.map2
+ (fun (id,_) (name, ty, bo) ->
+ (id, name, aux context ty, aux (tys@context) bo)
+ ) tys funs
+ )
+ in
+ aux
+;;
+
+let plain_acic_object_of_cic_object obj =
+ let module C = Cic in
+ let mk_fresh_id =
+ let id = ref 0 in
+ function () -> incr id; "it" ^ string_of_int !id
+ in
+ match obj with
+ C.Constant (id,Some bo,ty,params,attrs) ->
+ let abo = plain_acic_term_of_cic_term [] bo in
+ let aty = plain_acic_term_of_cic_term [] ty in
+ C.AConstant
+ ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
+ | C.Constant (id,None,ty,params,attrs) ->
+ let aty = plain_acic_term_of_cic_term [] ty in
+ C.AConstant
+ ("mettereaposto",None,id,None,aty,params,attrs)
+ | C.Variable (id,bo,ty,params,attrs) ->
+ let abo =
+ match bo with
+ None -> None
+ | Some bo -> Some (plain_acic_term_of_cic_term [] bo)
+ in
+ let aty = plain_acic_term_of_cic_term [] ty in
+ C.AVariable
+ ("mettereaposto",id,abo,aty,params,attrs)
+ | C.CurrentProof _ -> assert false
+ | C.InductiveDefinition (tys,params,paramsno,attrs) ->
+ let context =
+ List.map
+ (fun (name,_,arity,_) ->
+ mk_fresh_id (), Some (C.Name name, C.Decl arity)) tys in
+ let atys =
+ List.map2
+ (fun (id,_) (name,inductive,ty,cons) ->
+ let acons =
+ List.map
+ (function (name,ty) ->
+ (name,
+ plain_acic_term_of_cic_term context ty)
+ ) cons
+ in
+ (id,name,inductive,plain_acic_term_of_cic_term [] ty,acons)
+ ) context tys
+ in
+ C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
+;;
;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term ~ids_to_inner_sorts =
- let find_sort id =
- Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
+let print_term ?ids_to_inner_sorts =
+ let find_sort name id =
+ match ids_to_inner_sorts with
+ None -> []
+ | Some ids_to_inner_sorts ->
+ [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)]
in
let rec aux =
let module C = Cic in
let module U = UriManager in
function
C.ARel (id,idref,n,b) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
X.xml_empty "REL"
- [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
- None,"idref",idref ; None,"sort",sort]
+ (sort @
+ [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
+ None,"idref",idref])
| C.AVar (id,uri,exp_named_subst) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
aux_subst uri
(X.xml_empty "VAR"
- [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
+ (sort @ [None,"uri",U.string_of_uri uri;None,"id",id]))
exp_named_subst
| C.AMeta (id,n,l) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
X.xml_nempty "META"
- [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
+ (sort @ [None,"no",(string_of_int n) ; None,"id",id])
(List.fold_left
(fun i t ->
match t with
| t -> [],t
in
let prods,t = eat_prods prods in
- let sort = find_sort last_id in
- X.xml_nempty "PROD" [None,"type",sort]
+ let sort = find_sort "type" last_id in
+ X.xml_nempty "PROD" sort
[< List.fold_left
(fun i (id,binder,s) ->
- let sort = find_sort (Cic2acic.source_id_of_id id) in
+ let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
let attrs =
- (None,"id",id)::(None,"type",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"binder",b]
+ sort @ ((None,"id",id)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> [None,"binder",b])
in
[< i ; X.xml_nempty "decl" attrs (aux s) >]
) [< >] prods ;
X.xml_nempty "target" [] (aux t)
>]
| C.ACast (id,v,t) ->
- let sort = find_sort id in
- X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
+ let sort = find_sort "sort" id in
+ X.xml_nempty "CAST" (sort @ [None,"id",id])
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
>]
| t -> [],t
in
let lambdas,t = eat_lambdas lambdas in
- let sort = find_sort last_id in
- X.xml_nempty "LAMBDA" [None,"sort",sort]
+ let sort = find_sort "sort" last_id in
+ X.xml_nempty "LAMBDA" sort
[< List.fold_left
(fun i (id,binder,s) ->
- let sort = find_sort (Cic2acic.source_id_of_id id) in
+ let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
let attrs =
- (None,"id",id)::(None,"type",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"binder",b]
+ sort @ ((None,"id",id)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> [None,"binder",b])
in
[< i ; X.xml_nempty "decl" attrs (aux s) >]
) [< >] lambdas ;
| t -> [],t
in
let letins,t = eat_letins letins in
- let sort = find_sort last_id in
- X.xml_nempty "LETIN" [None,"sort",sort]
+ let sort = find_sort "sort" last_id in
+ X.xml_nempty "LETIN" sort
[< List.fold_left
(fun i (id,binder,s) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
let attrs =
- (None,"id",id)::(None,"sort",sort)::
- match binder with
- C.Anonymous -> []
- | C.Name b -> [None,"binder",b]
+ sort @ ((None,"id",id)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> [None,"binder",b])
in
[< i ; X.xml_nempty "def" attrs (aux s) >]
) [< >] letins ;
X.xml_nempty "target" [] (aux t)
>]
| C.AAppl (id,li) ->
- let sort = find_sort id in
- X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
+ let sort = find_sort "sort" id in
+ X.xml_nempty "APPLY" (sort @ [None,"id",id])
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
| C.AConst (id,uri,exp_named_subst) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
aux_subst uri
(X.xml_empty "CONST"
- [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
+ (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id])
) exp_named_subst
| C.AMutInd (id,uri,i,exp_named_subst) ->
aux_subst uri
None, "id", id]
) exp_named_subst
| C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
aux_subst uri
(X.xml_empty "MUTCONSTRUCT"
- [None,"uri", (U.string_of_uri uri) ;
- None,"noType",(string_of_int i) ;
- None,"noConstr",(string_of_int j) ;
- None,"id",id ; None,"sort",sort]
+ (sort @
+ [None,"uri", (U.string_of_uri uri) ;
+ None,"noType",(string_of_int i) ;
+ None,"noConstr",(string_of_int j) ;
+ None,"id",id])
) exp_named_subst
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
X.xml_nempty "MUTCASE"
- [None,"uriType",(U.string_of_uri uri) ;
- None,"noType", (string_of_int typeno) ;
- None,"id", id ; None,"sort",sort]
+ (sort @
+ [None,"uriType",(U.string_of_uri uri) ;
+ None,"noType", (string_of_int typeno) ;
+ None,"id", id])
[< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
List.fold_right
patterns [<>]
>]
| C.AFix (id, no, funs) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
X.xml_nempty "FIX"
- [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
+ (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
[< List.fold_right
(fun (id,fi,ai,ti,bi) i ->
[< X.xml_nempty "FixFunction"
) funs [<>]
>]
| C.ACoFix (id,no,funs) ->
- let sort = find_sort id in
+ let sort = find_sort "sort" id in
X.xml_nempty "COFIX"
- [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
+ (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
[< List.fold_right
(fun (id,fi,ti,bi) i ->
[< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
in
Xml.xml_nempty "attributes" [] xml_attrs
-let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
- let find_sort id =
- Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
- in
+let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
C.Name n' ->
[None,"id",hid;None,"name",n']
| C.Anonymous -> [None,"id",hid])
- (print_term ids_to_inner_sorts t)
+ (print_term ?ids_to_inner_sorts t)
| Some (n,C.ADef t) ->
X.xml_nempty "Def"
(match n with
C.Name n' ->
[None,"id",hid;None,"name",n']
| C.Anonymous -> [None,"id",hid])
- (print_term ids_to_inner_sorts t)
+ (print_term ?ids_to_inner_sorts t)
| None -> X.xml_empty "Hidden" [None,"id",hid]
) ;
i
>]
) [< >] canonical_context ;
X.xml_nempty "Goal" []
- (print_term ids_to_inner_sorts t)
+ (print_term ?ids_to_inner_sorts t)
>]
>])
[< >] conjectures ;
- X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
+ X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >]
in
let xml_for_current_proof_type =
X.xml_nempty "ConstantType"
[None,"name",n ; None,"params",params' ; None,"id", id]
- (print_term ids_to_inner_sorts ty)
+ (print_term ?ids_to_inner_sorts ty)
in
let xmlbo =
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_nempty "ConstantBody"
[None,"for",UriManager.string_of_uri uri ;
None,"params",params' ; None,"id", id]
- [< print_term ids_to_inner_sorts bo >]
+ [< print_term ?ids_to_inner_sorts bo >]
>]
in
let xmlty =
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
X.xml_nempty "ConstantType"
[None,"name",n ; None,"params",params' ; None,"id", id]
- [< xml_attrs; print_term ids_to_inner_sorts ty >]
+ [< xml_attrs; print_term ?ids_to_inner_sorts ty >]
>]
in
xmlty, xmlbo
match bo with
None -> [< >]
| Some bo ->
- X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+ X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >]
in
let aobj =
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_nempty "Variable"
[None,"name",n ; None,"params",params' ; None,"id", id]
[< xml_attrs; xmlbo;
- X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+ X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty)
>]
>]
in
None,"inductive",(string_of_bool finite)
]
[< X.xml_nempty "arity" []
- (print_term ids_to_inner_sorts arity) ;
+ (print_term ?ids_to_inner_sorts arity) ;
(List.fold_left
(fun i (name,lc) ->
[< i ;
X.xml_nempty "Constructor"
[None,"name",name]
- (print_term ids_to_inner_sorts lc)
+ (print_term ?ids_to_inner_sorts lc)
>]) [<>] cons
)
>]
[< x ;
X.xml_nempty "TYPE" [None,"of",id]
[< X.xml_nempty "synthesized" []
- [< print_term ids_to_inner_sorts synty >] ;
+ [< print_term ~ids_to_inner_sorts synty >] ;
match expty with
None -> [<>]
| Some expty' -> X.xml_nempty "expected" []
- [< print_term ids_to_inner_sorts expty' >]
+ [< print_term ~ids_to_inner_sorts expty' >]
>]
>]
) ids_to_inner_types [<>]
projects / helm.git / commitdiff