exception ImpossiblePossible;;
exception NotImplemented;;
-let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
+
+let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";;
+
+let param_attribute_of_params params =
+ String.concat " " (List.map UriManager.string_of_uri params)
+;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ~ids_to_inner_sorts =
+let print_term ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
function
- C.ARel (id,n,b) ->
+ C.ARel (id,idref,n,b) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_empty "REL"
- ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
- | C.AVar (id,uri) ->
- let vdepth = U.depth_of_uri uri
- and cdepth = U.depth_of_uri curi
- and sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "VAR"
- ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
- (U.name_of_uri uri) ;
- "id",id ; "sort",sort]
+ ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ;
+ "sort",sort]
+ | C.AVar (id,uri,exp_named_subst) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ aux_subst uri
+ (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort])
+ exp_named_subst
| C.AMeta (id,n,l) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
in
X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
| C.AImplicit _ -> raise NotImplemented
- | C.AProd (id,C.Anonimous,s,t) ->
- let ty = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "PROD" ["id",id ; "type",ty]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" [] (aux t)
- >]
- | C.AProd (xid,C.Name id,s,t) ->
- let ty = Hashtbl.find ids_to_inner_sorts xid in
- X.xml_nempty "PROD" ["id",xid ; "type",ty]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" ["binder",id] (aux t)
- >]
+ | C.AProd (last_id,_,_,_) as prods ->
+ let rec eat_prods =
+ function
+ C.AProd (id,n,s,t) ->
+ let prods,t' = eat_prods t in
+ (id,n,s)::prods,t'
+ | t -> [],t
+ in
+ let prods,t = eat_prods prods in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "PROD" ["type",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("type",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["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 = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "CAST" ["id",id ; "sort",sort]
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
>]
- | C.ALambda (id,C.Anonimous,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" [] (aux t)
- >]
- | C.ALambda (xid,C.Name id,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts xid in
- X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" ["binder",id] (aux t)
- >]
- | C.ALetIn (xid,C.Anonimous,s,t) ->
+ | C.ALambda (last_id,_,_,_) as lambdas ->
+ let rec eat_lambdas =
+ function
+ C.ALambda (id,n,s,t) ->
+ let lambdas,t' = eat_lambdas t in
+ (id,n,s)::lambdas,t'
+ | t -> [],t
+ in
+ let lambdas,t = eat_lambdas lambdas in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LAMBDA" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("type",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "decl" attrs (aux s) >]
+ ) [< >] lambdas ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | C.ALetIn (xid,C.Anonymous,s,t) ->
assert false
- | C.ALetIn (xid,C.Name id,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts xid in
- X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
- [< X.xml_nempty "term" [] (aux s) ;
- X.xml_nempty "letintarget" ["binder",id] (aux t)
- >]
+ | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ let rec eat_letins =
+ function
+ C.ALetIn (id,n,s,t) ->
+ let letins,t' = eat_letins t in
+ (id,n,s)::letins,t'
+ | t -> [],t
+ in
+ let letins,t = eat_letins letins in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LETIN" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("sort",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "def" attrs (aux s) >]
+ ) [< >] letins ;
+ X.xml_nempty "target" [] (aux t)
+ >]
| C.AAppl (id,li) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "APPLY" ["id",id ; "sort",sort]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
- | C.AConst (id,uri,_) ->
+ | C.AConst (id,uri,exp_named_subst) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "CONST"
- ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
- | C.AMutInd (id,uri,_,i) ->
- X.xml_empty "MUTIND"
- ["uri", (U.string_of_uri uri) ;
- "noType",(string_of_int i) ;
- "id",id]
- | C.AMutConstruct (id,uri,_,i,j) ->
+ aux_subst uri
+ (X.xml_empty "CONST"
+ ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
+ ) exp_named_subst
+ | C.AMutInd (id,uri,i,exp_named_subst) ->
+ aux_subst uri
+ (X.xml_empty "MUTIND"
+ ["uri", (U.string_of_uri uri) ;
+ "noType",(string_of_int i) ;
+ "id",id]
+ ) exp_named_subst
+ | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_empty "MUTCONSTRUCT"
- ["uri", (U.string_of_uri uri) ;
- "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
- "id",id ; "sort",sort]
- | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
+ aux_subst uri
+ (X.xml_empty "MUTCONSTRUCT"
+ ["uri", (U.string_of_uri uri) ;
+ "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
+ "id",id ; "sort",sort]
+ ) exp_named_subst
+ | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
X.xml_nempty "MUTCASE"
["uriType",(U.string_of_uri uri) ;
X.xml_nempty "FIX"
["noFun", (string_of_int no) ; "id",id ; "sort",sort]
[< List.fold_right
- (fun (fi,ai,ti,bi) i ->
+ (fun (id,fi,ai,ti,bi) i ->
[< X.xml_nempty "FixFunction"
- ["name", fi; "recIndex", (string_of_int ai)]
+ ["id",id ; "name", fi ; "recIndex", (string_of_int ai)]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
X.xml_nempty "COFIX"
["noFun", (string_of_int no) ; "id",id ; "sort",sort]
[< List.fold_right
- (fun (fi,ti,bi) i ->
- [< X.xml_nempty "CofixFunction" ["name", fi]
+ (fun (id,fi,ti,bi) i ->
+ [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
[< X.xml_nempty "type" [] [< aux ti >] ;
X.xml_nempty "body" [] [< aux bi >]
>] ;
>]
) funs [<>]
>]
- in
- aux
+ and aux_subst buri target subst =
+(*CSC: I have now no way to assign an ID to the explicit named substitution *)
+ let id = None in
+ if subst = [] then
+ target
+ else
+ Xml.xml_nempty "instantiate"
+ (match id with None -> [] | Some id -> ["id",id])
+ [< target ;
+ List.fold_left
+ (fun i (uri,arg) ->
+ let relUri =
+ let buri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
+ let uri_frags =
+ Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
+ let rec find_relUri buri_frags uri_frags =
+ match buri_frags,uri_frags with
+ [_], _ -> String.concat "/" uri_frags
+ | he1::tl1, he2::tl2 ->
+ assert (he1 = he2) ;
+ find_relUri tl1 tl2
+ | _,_ -> assert false (* uri is not relative to buri *)
+ in
+ find_relUri buri_frags uri_frags
+ in
+ [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
+ ) [<>] subst
+ >]
+ in
+ aux
;;
exception NotImplemented;;
-(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ~ids_to_inner_sorts =
+let print_object uri ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
function
- C.ACurrentProof (id,n,conjectures,bo,ty) ->
- X.xml_nempty "CurrentProof" ["name",n ; "id", id]
- [< List.fold_left
- (fun i (cid,n,canonical_context,t) ->
- [< i ;
- X.xml_nempty "Conjecture"
- ["id", cid ; "no",(string_of_int n)]
- [< List.fold_left
- (fun i (hid,t) ->
- [< (match t with
- Some (n,C.ADecl t) ->
- X.xml_nempty "Decl"
- (match n with
- C.Name n' -> ["id",hid;"name",n']
- | C.Anonimous -> ["id",hid])
- (print_term curi ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
- X.xml_nempty "Def"
- (match n with
- C.Name n' -> ["id",hid;"name",n']
- | C.Anonimous -> ["id",hid])
- (print_term curi ids_to_inner_sorts t)
- | None -> X.xml_empty "Hidden" ["id",hid]
- ) ;
- i
- >]
- ) [< >] canonical_context ;
- X.xml_nempty "Goal" []
- (print_term curi ids_to_inner_sorts t)
- >]
- >])
- [<>] conjectures ;
- X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
- X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
- | C.ADefinition (id,n,bo,ty,C.Actual params) ->
- let params' =
- 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 ""
+ C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xml_for_current_proof_body =
+(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
+(*CSC: I think so. Not implemented yet. *)
+ X.xml_nempty "CurrentProof"
+ ["of",UriManager.string_of_uri uri ; "id", id]
+ [< List.fold_left
+ (fun i (cid,n,canonical_context,t) ->
+ [< i ;
+ X.xml_nempty "Conjecture"
+ ["id", cid ; "no",(string_of_int n)]
+ [< List.fold_left
+ (fun i (hid,t) ->
+ [< (match t with
+ Some (n,C.ADecl t) ->
+ X.xml_nempty "Decl"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonymous -> ["id",hid])
+ (print_term ids_to_inner_sorts t)
+ | Some (n,C.ADef t) ->
+ X.xml_nempty "Def"
+ (match n with
+ C.Name n' -> ["id",hid;"name",n']
+ | C.Anonymous -> ["id",hid])
+ (print_term ids_to_inner_sorts t)
+ | None -> X.xml_empty "Hidden" ["id",hid]
+ ) ;
+ i
+ >]
+ ) [< >] canonical_context ;
+ X.xml_nempty "Goal" []
+ (print_term ids_to_inner_sorts t)
+ >]
+ >])
+ [<>] (List.rev conjectures) ;
+ X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
+ in
+ let xml_for_current_proof_type =
+ X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id]
+ (print_term ids_to_inner_sorts ty)
+ in
+ let xmlbo =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
+ xml_for_current_proof_body
+ >] in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
+ xml_for_current_proof_type
+ >]
+ in
+ xmlty, Some xmlbo
+ | C.AConstant (id,idbody,n,bo,ty,params) ->
+ let params' = param_attribute_of_params params in
+ let xmlbo =
+ match bo with
+ None -> None
+ | Some bo ->
+ Some
+ [< X.xml_cdata
+ "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata
+ ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
+ X.xml_nempty "ConstantBody"
+ ["for",UriManager.string_of_uri uri ; "params",params' ;
+ "id", id]
+ [< print_term ids_to_inner_sorts bo >]
+ >]
+ in
+ let xmlty =
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
+ X.xml_nempty "ConstantType"
+ ["name",n ; "params",params' ; "id", id]
+ [< print_term ids_to_inner_sorts ty >]
+ >]
in
- X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
- [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
- X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
- | C.ADefinition _ -> assert false
+ xmlty, xmlbo
| _ -> raise NotImplemented
in
aux
(fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
[< x ;
X.xml_nempty "TYPE" ["of",id]
- [< print_term curi ids_to_inner_sorts synty ;
+ [< print_term ids_to_inner_sorts synty ;
match expty with
None -> [<>]
- | Some expty' -> print_term curi ids_to_inner_sorts expty'
+ | Some expty' -> print_term ids_to_inner_sorts expty'
>]
>]
) ids_to_inner_types [<>]
exception NotImplemented
val print_term :
- UriManager.uri ->
ids_to_inner_sorts: (string, string) Hashtbl.t ->
Cic.annterm -> Xml.token Stream.t
val print_object :
UriManager.uri ->
ids_to_inner_sorts: (string, string) Hashtbl.t ->
- Cic.annobj -> Xml.token Stream.t
+ Cic.annobj -> Xml.token Stream.t * Xml.token Stream.t option
val print_inner_types :
UriManager.uri ->
{annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;
+let gen_id seed =
+ let res = "i" ^ string_of_int !seed in
+ incr seed ;
+ res
+;;
+
let fresh_id seed ids_to_terms ids_to_father_ids =
fun father t ->
- let res = "i" ^ string_of_int !seed in
- incr seed ;
+ let res = gen_id seed in
Hashtbl.add ids_to_father_ids res father ;
Hashtbl.add ids_to_terms res t ;
res
;;
let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- ids_to_inner_types metasenv context t expectedty
+ ids_to_inner_types metasenv context idrefs t expectedty
=
let module D = DoubleTypeInference in
let module T = CicTypeChecker in
let terms_to_types =
D.double_type_of metasenv context t expectedty
in
- let rec aux computeinnertypes father context tt =
+ let rec aux computeinnertypes father context idrefs tt =
let fresh_id'' = fresh_id' father tt in
(*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
let aux' = aux computeinnertypes (Some fresh_id'') in
match expected with
None -> None,false
| Some expectedty' ->
- Some (aux false (Some fresh_id'') context expectedty'),true
+ Some
+ (aux false (Some fresh_id'') context idrefs expectedty'),
+ true
in
Some
{annsynthesized =
- aux false (Some fresh_id'') context synthesized ;
+ aux false (Some fresh_id'') context idrefs synthesized ;
annexpected = annexpected
}, expected_available
else
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
- C.ARel (fresh_id'', n, id)
- | C.Var uri ->
+ C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
+ | C.Var (uri,exp_named_subst) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
- C.AVar (fresh_id'', uri)
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux' context idrefs t)) exp_named_subst
+ in
+ C.AVar (fresh_id'', uri,exp_named_subst')
| C.Meta (n,l) ->
let (_,canonical_context,_) =
List.find (function (m,_,_) -> n = m) metasenv
(fun ct t ->
match (ct, t) with
| None, _ -> None
- | _, Some t -> Some (aux' context t)
+ | _, Some t -> Some (aux' context idrefs t)
| Some _, None -> assert false (* due to typing rules *))
canonical_context l))
| C.Sort s -> C.ASort (fresh_id'', s)
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.ACast (fresh_id'', aux' context v, aux' context t)
+ C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
| C.Prod (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id''
(string_of_sort innertype) ;
C.AProd
- (fresh_id'', n, aux' context s,
- aux' ((Some (n, C.Decl s))::context) t)
+ (fresh_id'', n, aux' context idrefs s,
+ aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
| C.Lambda (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id''
end ;
C.ALambda
- (fresh_id'',n, aux' context s,
- aux' ((Some (n, C.Decl s)::context)) t)
+ (fresh_id'',n, aux' context idrefs s,
+ aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
| C.LetIn (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ALetIn
- (fresh_id'', n, aux' context s,
- aux' ((Some (n, C.Def s))::context) t)
+ (fresh_id'', n, aux' context idrefs s,
+ aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t)
| C.Appl l ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.AAppl (fresh_id'', List.map (aux' context) l)
- | C.Const (uri,cn) ->
+ C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
+ | C.Const (uri,exp_named_subst) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
- C.AConst (fresh_id'', uri, cn)
- | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
- | C.MutConstruct (uri,cn,tyno,consno) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux' context idrefs 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 idrefs t)) exp_named_subst
+ in
+ C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" && expected_available then
add_inner_type fresh_id'' ;
- C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
- | C.MutCase (uri, cn, tyno, outty, term, patterns) ->
+ let exp_named_subst' =
+ List.map
+ (function i,t -> i, (aux' context idrefs t)) exp_named_subst
+ in
+ C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
+ | C.MutCase (uri, tyno, outty, term, patterns) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
if innersort = "Prop" then
add_inner_type fresh_id'' ;
- C.AMutCase (fresh_id'', uri, cn, tyno, aux' context outty,
- aux' context term, List.map (aux' context) patterns)
+ C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
+ aux' context idrefs term, List.map (aux' context idrefs) patterns)
| C.Fix (funno, funs) ->
+ let fresh_idrefs =
+ List.map (function _ -> gen_id seed) funs in
+ let new_idrefs = List.rev fresh_idrefs @ idrefs in
let tys =
List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
in
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.AFix (fresh_id'', funno,
- List.map
- (fun (name, indidx, ty, bo) ->
- (name, indidx, aux' context ty, aux' (tys@context) bo)
- ) funs
+ List.map2
+ (fun id (name, indidx, ty, bo) ->
+ (id, name, indidx, aux' context idrefs ty,
+ aux' (tys@context) new_idrefs bo)
+ ) fresh_idrefs funs
)
| C.CoFix (funno, funs) ->
+ let fresh_idrefs =
+ List.map (function _ -> gen_id seed) funs in
+ let new_idrefs = List.rev fresh_idrefs @ idrefs in
let tys =
List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
in
if innersort = "Prop" then
add_inner_type fresh_id'' ;
C.ACoFix (fresh_id'', funno,
- List.map
- (fun (name, ty, bo) ->
- (name, aux' context ty, aux' (tys@context) bo)
- ) funs
+ List.map2
+ (fun id (name, ty, bo) ->
+ (id, name, aux' context idrefs ty,
+ aux' (tys@context) new_idrefs bo)
+ ) fresh_idrefs funs
)
in
- aux true None context t
+ aux true None context idrefs t
;;
-let acic_of_cic_context metasenv context t =
+let acic_of_cic_context metasenv context idrefs t =
let ids_to_terms = Hashtbl.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
let seed = ref 0 in
acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- ids_to_inner_types metasenv context t,
+ ids_to_inner_types metasenv context idrefs t,
ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;
let acic_term_of_cic_term_context' =
acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
ids_to_inner_types in
- let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] in
+ let acic_term_of_cic_term' = acic_term_of_cic_term_context' [] [] [] in
let aobj =
match obj with
- C.Definition (id,bo,ty,params) ->
+ C.Constant (id,Some bo,ty,params) ->
let abo = acic_term_of_cic_term' bo (Some ty) in
let aty = acic_term_of_cic_term' ty None in
- C.ADefinition ("mettereaposto",id,abo,aty,(Cic.Actual params))
- | C.Axiom (id,ty,params) -> raise NotImplemented
- | C.Variable (id,bo,ty) -> raise NotImplemented
- | C.CurrentProof (id,conjectures,bo,ty) ->
+ C.AConstant
+ ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
+ | C.Constant (id,None,ty,params) -> raise NotImplemented
+ | C.Variable (id,bo,ty,params) -> raise NotImplemented
+ | C.CurrentProof (id,conjectures,bo,ty,params) ->
let aconjectures =
List.map
(function (i,canonical_context,term) as conjecture ->
let cid = "c" ^ string_of_int !conjectures_seed in
Hashtbl.add ids_to_conjectures cid conjecture ;
incr conjectures_seed ;
- let acanonical_context =
- let rec aux =
+ let idrefs',revacanonical_context =
+ let rec aux context idrefs =
function
- [] -> []
+ [] -> idrefs,[]
| hyp::tl ->
let hid = "h" ^ string_of_int !hypotheses_seed in
+ let new_idrefs = hid::idrefs in
Hashtbl.add ids_to_hypotheses hid hyp ;
incr hypotheses_seed ;
match hyp with
(Some (n,C.Decl t)) ->
+ let final_idrefs,atl =
+ aux (hyp::context) new_idrefs tl in
let at =
- acic_term_of_cic_term_context' conjectures tl t None
+ acic_term_of_cic_term_context'
+ conjectures context idrefs t None
in
- (hid,Some (n,C.ADecl at))::(aux tl)
+ final_idrefs,(hid,Some (n,C.ADecl at))::atl
| (Some (n,C.Def t)) ->
+ let final_idrefs,atl =
+ aux (hyp::context) new_idrefs tl in
let at =
- acic_term_of_cic_term_context' conjectures tl t None
+ acic_term_of_cic_term_context'
+ conjectures context idrefs t None
in
- (hid,Some (n,C.ADef at))::(aux tl)
- | None -> (hid,None)::(aux tl)
+ final_idrefs,(hid,Some (n,C.ADef at))::atl
+ | None ->
+ let final_idrefs,atl =
+ aux (hyp::context) new_idrefs tl
+ in
+ final_idrefs,(hid,None)::atl
in
- aux canonical_context
+ aux [] [] (List.rev canonical_context)
in
let aterm =
- acic_term_of_cic_term_context' conjectures canonical_context
- term None
+ acic_term_of_cic_term_context' conjectures
+ canonical_context idrefs' term None
in
- (cid,i,acanonical_context,aterm)
+ (cid,i,(List.rev revacanonical_context),aterm)
) conjectures in
- let abo = acic_term_of_cic_term_context' conjectures [] bo (Some ty) in
- let aty = acic_term_of_cic_term_context' conjectures [] ty None in
- C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
+ let abo =
+ acic_term_of_cic_term_context' conjectures [] [] bo (Some ty) in
+ let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
+ C.ACurrentProof
+ ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
| C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
in
aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
(Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
Cic.metasenv -> (* metasenv *)
Cic.context -> (* context *)
+ Cic.id list -> (* idrefs *)
Cic.term -> (* term *)
Cic.term option -> (* expected type *)
Cic.annterm (* annotated term *)
let module S = CicSubstitution in
let module C = Cic in
function
- C.Rel _
- | C.Var _ as t -> t
+ C.Rel _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst)
| C.Meta (n,l) ->
C.Meta (n,
List.map
head_beta_reduce (C.Appl (he'::tl))
| C.Appl l ->
C.Appl (List.map head_beta_reduce l)
- | C.Const _ as t -> t
- | C.MutInd _
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cno,i,outt,t,pl) ->
- C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
List.map head_beta_reduce pl)
| C.Fix (i,fl) ->
let fl' =
if t = t' then true
else
match t, t' with
- C.Rel _, C.Rel _
- | C.Var _, C.Var _
- | C.Meta _, C.Meta _
- | C.Sort _, C.Sort _
- | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
+ UriManager.eq uri uri' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
| C.Cast (te,ty), C.Cast (te',ty') ->
syntactic_equality te te' &&
syntactic_equality ty ty'
syntactic_equality t t'
| C.Appl l, C.Appl l' ->
List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
- | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
- | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
- UriManager.eq uri uri' && i = i'
- | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
- UriManager.eq uri uri' && i = i' && j = j'
- | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
+ UriManager.eq uri uri' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
+ UriManager.eq uri uri' && i = i' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutConstruct (uri,i,j,exp_named_subst),
+ C.MutConstruct (uri',i',j',exp_named_subst') ->
+ UriManager.eq uri uri' && i = i' && j = j' &&
+ syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
+ | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
UriManager.eq sp sp' && i = i' &&
syntactic_equality outt outt' &&
syntactic_equality t t' &&
b &&
syntactic_equality ty ty' &&
syntactic_equality bo bo') true fl fl'
- | _,_ -> false
+ | _, _ -> false (* we already know that t != t' *)
+ and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
+ List.fold_left2
+ (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
+ exp_named_subst1 exp_named_subst2
in
try
syntactic_equality t t'
| (_,_) -> raise ListTooShort
;;
-let cooked_type_of_constant uri cookingsno =
+let 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 ->
raise (NotWellTyped "Reference to an unchecked constant")
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))
;;
let module C = Cic in
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
+ match CicEnvironment.is_type_checked uri with
+ CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
| CicEnvironment.UncheckedObj (C.Variable _) ->
raise (NotWellTyped "Reference to an unchecked variable")
| _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
;;
-let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+let 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 ->
raise (NotWellTyped "Reference to an unchecked inductive type")
| _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
;;
-let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+let 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 ->
raise (NotWellTyped "Reference to an unchecked constructor")
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))
;;
with
_ -> raise (NotWellTyped "Not a close term")
)
- | C.Var uri -> type_of_variable uri
+ | C.Var (uri,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
| C.Meta (n,l) ->
(* Let's visit all the subterms that will not be visited later *)
let (_,canonical_context,_) =
in
eat_prods context hetype tlbody_and_type
| C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
- | C.Const (uri,cookingsno) ->
- cooked_type_of_constant uri cookingsno
- | C.MutInd (uri,cookingsno,i) ->
- cooked_type_of_mutual_inductive_defs uri cookingsno i
- | C.MutConstruct (uri,cookingsno,i,j) ->
- let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
- cty
- | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
+ | C.Const (uri,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+ | C.MutInd (uri,i,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_defs uri i)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ visit_exp_named_subst context uri exp_named_subst ;
+ CicSubstitution.subst_vars exp_named_subst
+ (type_of_mutual_inductive_constr uri i j)
+ | C.MutCase (uri,i,outtype,term,pl) ->
let outsort = type_of_aux context outtype None 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 ->
+ C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
(false, 1)
- | C.Appl ((C.MutInd (uri',_,i')) :: _)
+ | 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) =
let type_of_term =
CicTypeChecker.type_of_aux' metasenv context term
in
(Some (head_beta_reduce type_of_term)))
with
(*CSC manca il caso dei CAST *)
- C.MutInd (uri',_,i') ->
+ C.MutInd (uri',i',exp_named_subst) ->
(* Checks suppressed *)
- [],[]
- | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+ [],[],exp_named_subst
+ | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
+ let params,args =
split tl (List.length tl - k)
+ in params,args,exp_named_subst
| _ ->
raise (NotWellTyped "MutCase: the term is not an inductive one")
in
(* Checks suppressed *)
(* Let's visit all the subterms that will not be visited later *)
let (cl,parsno) =
- match CicEnvironment.get_cooked_obj uri cookingsno with
+ match CicEnvironment.get_cooked_obj uri with
C.InductiveDefinition (tl,_,parsno) ->
let (_,_,_,cl) = List.nth tl i in (cl,parsno)
| _ ->
in
let _ =
List.fold_left
- (fun j (p,(_,c,_)) ->
+ (fun j (p,(_,c)) ->
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
let expectedtype =
type_of_branch context parsno need_dummy outtype cons
CicHash.add subterms_to_types t types ;
res
+ and visit_exp_named_subst context uri exp_named_subst =
+ let uris_and_types =
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,_,_,params)
+ | Cic.CurrentProof (_,_,_,_,params)
+ | Cic.Variable (_,_,_,params)
+ | Cic.InductiveDefinition (_,params,_) ->
+ List.map
+ (function uri ->
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Variable (_,None,ty,_) -> uri,ty
+ | _ -> assert false (* the theorem is well-typed *)
+ ) params
+ in
+ let rec check uris_and_types subst =
+ match uris_and_types,subst with
+ _,[] -> []
+ | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
+ ignore (type_of_aux context t (Some ty)) ;
+ let tytl' =
+ List.map
+ (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
+ in
+ check tytl' substtl
+ | _,_ -> assert false (* the theorem is well-typed *)
+ in
+ check uris_and_types exp_named_subst
+
and sort_of_prod context (name,s) (t1, t2) =
let module C = Cic in
let t1' = CicReduction.whd context t1 in
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)
-alias and /Coq/Init/Logic/Conjunction/and.ind#1/1
-alias conj /Coq/Init/Logic/Conjunction/and.ind#1/1/1
+alias and /Coq/Init/Logic/and.ind#1/1
+alias conj /Coq/Init/Logic/and.ind#1/1/1
-alias or /Coq/Init/Logic/Disjunction/or.ind#1/1
-alias or_introl /Coq/Init/Logic/Disjunction/or.ind#1/1/1
-alias or_intror /Coq/Init/Logic/Disjunction/or.ind#1/1/2
+alias or /Coq/Init/Logic/or.ind#1/1
+alias or_introl /Coq/Init/Logic/or.ind#1/1/1
+alias or_intror /Coq/Init/Logic/or.ind#1/1/2
!A:Prop.!B:Prop.!H:(and A B).(or A B)
alias nat /Coq/Init/Datatypes/nat.ind#1/1
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
alias plus /Coq/Init/Peano/plus.con
alias not /Coq/Init/Logic/not.con
(eq nat (\x:nat.\y:nat.O O O) (\x:nat.\y:nat.O O O))
/Coq/Init/Logic/f_equal2.con
-/Coq/Init/Logic/Equality/eq.ind#1/1/1
+/Coq/Init/Logic/eq.ind#1/1/1
(*
(le O (S O))
alias nat /Coq/Init/Datatypes/nat.ind#1/1
alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias refl_equal /Coq/Init/Logic/Equality/eq.ind#1/1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias refl_equal /Coq/Init/Logic/eq.ind#1/1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
+alias eq_ind_r /Coq/Init/Logic/eq_ind_r.con
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
alias plus /Coq/Init/Peano/plus.con
alias le /Coq/Init/Peano/le.ind#1/1
alias lt /Coq/Init/Peano/lt.con
alias not /Coq/Init/Logic/not.con
-alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias f_equal /Coq/Init/Logic/f_equal.con
alias le_trans /Coq/Arith/Le/le_trans.con
alias plus_n_O /Coq/Init/Peano/plus_n_O.con
-alias or /Coq/Init/Logic/Disjunction/or.ind#1/1
-alias or_ind /Coq/Init/Logic/Disjunction/or_ind.con
+alias or /Coq/Init/Logic/or.ind#1/1
+alias or_ind /Coq/Init/Logic/or_ind.con
(or (eq nat O O) (eq nat O O)) -> (lt O O)
alias False /Coq/Init/Logic/False.ind#1/1
alias False_ind /Coq/Init/Logic/False_ind.con
-alias and /Coq/Init/Logic/Conjunction/and.ind#1/1
-alias conj /Coq/Init/Logic/Conjunction/and.ind#1/1/1
-alias and_ind /Coq/Init/Logic/Conjunction/and_ind.con
+alias and /Coq/Init/Logic/and.ind#1/1
+alias conj /Coq/Init/Logic/and.ind#1/1/1
+alias and_ind /Coq/Init/Logic/and_ind.con
-alias or /Coq/Init/Logic/Disjunction/or.ind#1/1
-alias or_introl /Coq/Init/Logic/Disjunction/or.ind#1/1/1
-alias or_intror /Coq/Init/Logic/Disjunction/or.ind#1/1/2
-alias or_ind /Coq/Init/Logic/Disjunction/or_ind.con
+alias or /Coq/Init/Logic/or.ind#1/1
+alias or_introl /Coq/Init/Logic/or.ind#1/1/1
+alias or_intror /Coq/Init/Logic/or.ind#1/1/2
+alias or_ind /Coq/Init/Logic/or_ind.con
alias not /Coq/Init/Logic/not.con
alias nat /Coq/Init/Datatypes/nat.ind#1/1
alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias refl_equal /Coq/Init/Logic/Equality/eq.ind#1/1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias refl_equal /Coq/Init/Logic/eq.ind#1/1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
+alias eq_ind_r /Coq/Init/Logic/eq_ind_r.con
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
alias plus /Coq/Init/Peano/plus.con
alias le /Coq/Init/Peano/le.ind#1/1
alias lt /Coq/Init/Peano/lt.con
alias not /Coq/Init/Logic/not.con
-alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias f_equal /Coq/Init/Logic/f_equal.con
!n:nat.(eq nat (mult (S (S O)) n) O)
!n:nat.(eq nat (plus O n) (plus n O))
alias nat /Coq/Init/Datatypes/nat.ind#1/1
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
alias plus /Coq/Init/Peano/plus.con
alias le /Coq/Init/Peano/le.ind#1/1
alias lt /Coq/Init/Peano/lt.con
alias not /Coq/Init/Logic/not.con
-alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias f_equal /Coq/Init/Logic/f_equal.con
!n:nat.(eq nat (plus O n) (plus n O))
alias nat /Coq/Init/Datatypes/nat.ind#1/1
alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
-alias refl_equal /Coq/Init/Logic/Equality/eq.ind#1/1/1
-alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias eq /Coq/Init/Logic/eq.ind#1/1
+alias refl_equal /Coq/Init/Logic/eq.ind#1/1/1
+alias eq_ind /Coq/Init/Logic/eq_ind.con
+alias eq_ind_r /Coq/Init/Logic/eq_ind_r.con
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
alias plus /Coq/Init/Peano/plus.con
alias le /Coq/Init/Peano/le.ind#1/1
alias lt /Coq/Init/Peano/lt.con
alias not /Coq/Init/Logic/not.con
-alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias f_equal /Coq/Init/Logic/f_equal.con
alias le_trans /Coq/Arith/Le/le_trans.con
alias le_plus_plus /Coq/Arith/Plus/le_plus_plus.con
-alias eq /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eq /Coq/Init/Logic/eq.ind#1/1
alias nat /Coq/Init/Datatypes/nat.ind#1/1
alias O /Coq/Init/Datatypes/nat.ind#1/1/1
alias S /Coq/Init/Datatypes/nat.ind#1/1/2
Open:
-/Coq/Sets/Powerset_facts/Sets_as_an_algebra/Union_commutative.con
+/Coq/Sets/Powerset_facts/Union_commutative.con
We prove the conjunction again:
-alias Ensemble /Coq/Sets/Ensembles/Ensembles/Ensemble.con
-alias Union /Coq/Sets/Ensembles/Ensembles/Union.ind#1/1
-alias Included /Coq/Sets/Ensembles/Ensembles/Included.con
-alias and /Coq/Init/Logic/Conjunction/and.ind#1/1
+alias U /Coq/Sets/Ensembles/Ensembles/U.var
+alias V /Coq/Sets/Powerset_facts/Sets_as_an_algebra/U.var
+alias Ensemble /Coq/Sets/Ensembles/Ensemble.con
+alias Union /Coq/Sets/Ensembles/Union.ind#1/1
+alias Included /Coq/Sets/Ensembles/Included.con
+alias and /Coq/Init/Logic/and.ind#1/1
The two parts of the conjunction can be proved in the same way. So we
can make a Cut:
-!V:Set.!C:(Ensemble V).!D:(Ensemble V).(Included V (Union V C D)
-(Union V D C))
+!C:Ensemble{U:=V}.!D:Ensemble{U:=V}.
+ (Included{U:=V} (Union{U:=V} C D) (Union{U:=V} D C))
let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
let eq_ind_r,ty,t1,t2 =
match CicTypeChecker.type_of_aux' metasenv context equality with
- C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
- when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
+ C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
+ when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
let eq_ind_r =
C.Const
- (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
+ (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
in
eq_ind_r,ty,t1,t2
- | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
+ | C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
let eqT_ind_r =
C.Const
- (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
+ (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
in
eqT_ind_r,ty,t1,t2
| _ ->
let t1' = CicSubstitution.lift 1 t1 in
let gty'' =
ProofEngineReduction.replace_lifting
- ~equality:
- (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
+ ~equality:ProofEngineReduction.alpha_equivalence
~what:t1' ~with_what:(C.Rel 1) ~where:gty'
in
C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
*)
let rec string_of_term t =
match t with
- Cic.Cast (t1,t2) -> string_of_term t1
- |Cic.Const (u,boh) -> UriManager.string_of_uri u
- |Cic.Var (u) -> UriManager.string_of_uri u
+ Cic.Cast (t,_) -> string_of_term t
+ |Cic.Const (u,_) -> UriManager.string_of_uri u
+ |Cic.Var (u,_) -> UriManager.string_of_uri u
| _ -> "not_of_constant"
;;
*)
-let _eqT = Cic.MutInd(UriManager.uri_of_string
- "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
-let _False = Cic.MutInd (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
-let _not = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/not.con") 0;;
-let _R0 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
-let _R1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
-let _R = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
-let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
-let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
-let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
-let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
-let _Rfourier_le=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
-let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
-let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
-let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
-let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
-let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
-let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
-let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
-let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
-let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
-let _Rinv = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
- "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
-let _Rle = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
-let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
-let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
-let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
-let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
-let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
-let _Rlt = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
-let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
-let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
-let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
-let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-let _Rminus = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
-let _Rmult = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
-let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
-let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
- "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
-let _Ropp = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
-let _Rplus = Cic.Const (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-let _sym_eqT = Cic.Const(UriManager.uri_of_string
- "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+let _eqT =
+ Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [];;
+let _False =
+ Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [];;
+let _not =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") [];;
+let _R0 =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") [];;
+let _R1 =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") [];;
+let _R =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") [];;
+let _Rfourier_eqLR_to_le=
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [];;
+let _Rfourier_eqRL_to_le =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [];;
+let _Rfourier_ge_to_le =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [];;
+let _Rfourier_gt_to_lt =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [];;
+let _Rfourier_le =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con")[];;
+let _Rfourier_le_le =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con")
+ [];;
+let _Rfourier_le_lt =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con")
+ [] ;;
+let _Rfourier_lt =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") []
+;;
+let _Rfourier_lt_le =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con")
+ []
+;;
+let _Rfourier_lt_lt =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con")
+ []
+;;
+let _Rfourier_not_ge_lt =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [];;
+let _Rfourier_not_gt_le =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [];;
+let _Rfourier_not_le_gt =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [];;
+let _Rfourier_not_lt_ge =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [];;
+let _Rinv =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con")[];;
+let _Rinv_R1 =
+ Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [];;
+let _Rle =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") [];;
+let _Rle_mult_inv_pos =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [];;
+let _Rle_not_lt =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [];;
+let _Rle_zero_1 =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [];;
+let _Rle_zero_pos_plus1 =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [];;
+let _Rle_zero_zero =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con")
+ []
+;;
+let _Rlt =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [];;
+let _Rlt_mult_inv_pos =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [];;
+let _Rlt_not_le =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [];;
+let _Rlt_zero_1 =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [];;
+let _Rlt_zero_pos_plus1 =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [];;
+let _Rminus =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con")
+ []
+;;
+let _Rmult =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con")
+ []
+;;
+let _Rnot_le_le =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [];;
+let _Rnot_lt0 =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [];;
+let _Rnot_lt_lt =
+ Cic.Const
+ (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [];;
+let _Ropp =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") []
+;;
+let _Rplus =
+ Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") []
+;;
+let _sym_eqT =
+ Cic.Const
+ (UriManager.uri_of_string
+ "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") [];;
(******************************************************************************)
let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
*)
let prooffile = "/public/sacerdot/currentproof";;
+let prooffiletype = "/public/sacerdot/currentprooftype";;
(*CSC: the getter should handle the innertypes, not the FS *)
(*
let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
*)
let innertypesfile = "/public/sacerdot/innertypes";;
+let constanttypefile = "/public/sacerdot/constanttype";;
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
(* MISC FUNCTIONS *)
+let cic_textual_parser_uri_of_uri uri' =
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+ CicTextualParser0.ConUri (UriManager.uri_of_string uri')
+ else
+ if String.sub uri' (String.length uri' - 4) 4 = ".var" then
+ CicTextualParser0.VarUri (UriManager.uri_of_string uri')
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+ CicTextualParser0.IndTyUri (uri'',typeno)
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+ CicTextualParser0.IndConUri (uri'',typeno,consno)
+ )
+;;
+
+let term_of_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ match (cic_textual_parser_uri_of_uri uri) with
+ CTP.ConUri uri -> C.Const (uri,[])
+ | CTP.VarUri uri -> C.Var (uri,[])
+ | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
+ | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
+;;
+
let domImpl = Gdome.domImplementation ();;
let parseStyle name =
;;
let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
- let xml =
+(*CSC: ????????????????? *)
+ let xml, bodyxml =
Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
in
let xmlinnertypes =
Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
~ids_to_inner_types
in
- let input = Xml2Gdome.document_of_xml domImpl xml in
+ let input =
+ match bodyxml with
+ None -> Xml2Gdome.document_of_xml domImpl xml
+ | Some bodyxml' ->
+ Xml.pp xml (Some constanttypefile) ;
+ Xml2Gdome.document_of_xml domImpl bodyxml'
+ in
(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
(*CSC: local. *)
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
+ (*CSC: Wrong: [] is just plainly wrong *)
+ uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
in
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
+prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (RefreshProofException e)
;;
then
begin
(*CSC: Wrong: [] is just plainly wrong *)
- let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
+ let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
(*????
let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
-*)
let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
+*)
+let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
let save rendering_window () =
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
None -> assert false
| Some (uri, metasenv, bo, ty) ->
let currentproof =
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
+ (*CSC: Wrong: [] is just plainly wrong *)
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
Cic2acic.acic_object_of_cic_object currentproof
in
- let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
- let xml' =
- [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
- Xml.xml_cdata
- ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
- xml
- >]
- in
- Xml.pp ~quiet:true xml' (Some prooffile) ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof saved to " ^
- prooffile ^ "</h1>")
+ let xml, bodyxml =
+ match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
+ xml,Some bodyxml -> xml,bodyxml
+ | _,None -> assert false
+ in
+ Xml.pp ~quiet:true xml (Some prooffiletype) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof type saved to " ^
+ prooffiletype ^ "</h1>") ;
+ Xml.pp ~quiet:true bodyxml (Some prooffile) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof body saved to " ^
+ prooffile ^ "</h1>")
;;
(* Used to typecheck the loaded proofs *)
let typecheck_loaded_proof metasenv bo ty =
let module T = CicTypeChecker in
- (*CSC: bisogna controllare anche il metasenv!!! *)
+ ignore (
+ List.fold_left
+ (fun metasenv ((_,context,ty) as conj) ->
+ ignore (T.type_of_aux' metasenv context ty) ;
+ metasenv @ [conj]
+ ) [] metasenv) ;
ignore (T.type_of_aux' metasenv [] ty) ;
ignore (T.type_of_aux' metasenv [] bo)
;;
+(*CSC: ancora da implementare *)
let load rendering_window () =
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let output = (rendering_window#output : GMathView.math_view) in
let proofw = (rendering_window#proofw : GMathView.math_view) in
try
let uri = UriManager.uri_of_string "cic:/dummy.con" in
- match CicParser.obj_of_xml prooffile uri with
- Cic.CurrentProof (_,metasenv,bo,ty) ->
+ match CicParser.obj_of_xml prooffiletype (Some prooffile) with
+ Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
ProofEngine.proof :=
Some (uri, metasenv, bo, ty) ;
refresh_proof output ;
refresh_sequent proofw ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof loaded from " ^
+ ("<h1 color=\"Green\">Current proof type loaded from " ^
+ prooffiletype ^ "</h1>") ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof body loaded from " ^
prooffile ^ "</h1>")
| _ -> assert false
with
let output = (rendering_window#output : GMathView.math_view) in
let proofw = (rendering_window#proofw : GMathView.math_view) in
let inputlen = inputt#length in
- let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let input = inputt#get_chars 0 inputlen in
try
let uri = UriManager.uri_of_string ("cic:" ^ input) in
CicTypeChecker.typecheck uri ;
let metasenv,bo,ty =
- match CicEnvironment.get_cooked_obj uri 0 with
- Cic.Definition (_,bo,ty,_) -> [],bo,ty
- | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
- | Cic.Axiom _
+ match CicEnvironment.get_cooked_obj uri with
+ Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ | Cic.Constant _
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
| None -> None
) context
in
- (* Do something interesting *)
let lexbuf = Lexing.from_string input in
try
while true do
try
let ty = CicTypeChecker.type_of_aux' metasenv' context expr in
let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
+prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
scratch_window#show () ;
scratch_window#mmlwidget#load_tree ~dom:mml
with
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
;;
-let backward rendering_window () =
+let searchPattern rendering_window () =
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let inputt = (rendering_window#inputt : GEdit.text) in
let inputlen = inputt#length in
None -> ()
| Some metano ->
let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let result = MQueryGenerator.backward metasenv ey ty level in
+ let result = MQueryGenerator.searchPattern metasenv ey ty level in
let uris =
List.map
(function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
let html =
" <h1>Backward Query: </h1>" ^
" <h2>Levels: </h2> " ^
- MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
- " <pre>" ^ get_last_query result ^ "</pre>" in
+ MQueryGenerator.string_of_levels
+ (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
+ " <pre>" ^ get_last_query result ^ "</pre>"
+ in
output_html outputhtml html ;
- let uri' = user_uri_choice uris in
- inputt#delete_text 0 inputlen ;
- ignore ((inputt#insert_text uri') ~pos:0)
+ let uris',exc =
+ let rec filter_out =
+ function
+ [] -> [],""
+ | uri::tl ->
+ let tl',exc = filter_out tl in
+ try
+ if ProofEngine.can_apply (term_of_uri uri) then
+ uri::tl',exc
+ else
+ tl',exc
+ with
+ e ->
+ let exc' =
+ "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
+ uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
+ in
+ tl',exc'
+ in
+ filter_out uris
+ in
+ let html' =
+ " <h1>Objects that can actually be applied: </h1> " ^
+ String.concat "<br>" uris' ^ exc ^
+ " <h1>Number of false matches: " ^
+ string_of_int (List.length uris - List.length uris') ^ "</h1>"
+ in
+ output_html outputhtml html' ;
+ let uri' = user_uri_choice uris' in
+ inputt#delete_text 0 inputlen ;
+ ignore ((inputt#insert_text uri') ~pos:0)
with
e ->
output_html outputhtml
let locateb =
GButton.button ~label:"Locate"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
- let backwardb =
- GButton.button ~label:"Backward"
+ let searchpatternb =
+ GButton.button ~label:"SearchPattern"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
~packing:(vbox#pack ~padding:5) () in
ignore(openb#connect#clicked (open_ self)) ;
ignore(checkb#connect#clicked (check self scratch_window)) ;
ignore(locateb#connect#clicked (locate self)) ;
- ignore(backwardb#connect#clicked (backward self)) ;
+ ignore(searchpatternb#connect#clicked (searchPattern self)) ;
ignore(exactb#connect#clicked (exact self)) ;
ignore(applyb#connect#clicked (apply self)) ;
ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
;;
let _ =
- CicCooking.init () ;
if !usedb then
begin
- Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ;
+(*
+ Mqint.init "dbname=helm" ;
+*)
+ Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
CicTextualParser0.set_locate_object
(function id ->
let result = MQueryGenerator.locate id in
let uris =
List.map
- (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
- result in
- let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
+ (function uri,_ ->
+ wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ let html =
+ (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
+ in
begin
match !rendering_window with
None -> assert false
None
in
match uri with
- Some uri' ->
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
-(*CSC: what cooking number? Here I always use 0, which may be bugged *)
- Some (Cic.Const (UriManager.uri_of_string uri',0))
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
-(*CSC: what cooking number? Here I always use 0, which may be bugged *)
- Some (Cic.MutInd (uri'',0,typeno))
- with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
-(*CSC: what cooking number? Here I always use 0, which may be bugged *)
- Some (Cic.MutConstruct (uri'',0,typeno,consno))
- )
+ Some uri' -> Some (cic_textual_parser_uri_of_uri uri')
| None -> None
)
end ;
entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l
in
let rec inspect_term main l v term = match term with
- | Cic.Rel _ -> l
- | Cic.Meta (_, _) -> l
+ Cic.Rel _ -> l
+ | Cic.Meta _ -> l
| Cic.Sort _ -> l
| Cic.Implicit -> l
- | Cic.Var u -> inspect_uri main l u [] v term
- | Cic.Const (u, _) -> inspect_uri main l u [] v term
- | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term
- | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
+ | Cic.Var (u,exp_named_subst) ->
+ let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l' (v+1) exp_named_subst
+ | Cic.Const (u,exp_named_subst) ->
+ let l' = inspect_uri main l u [] v term in
+ inspect_exp_named_subst l' (v+1) exp_named_subst
+ | Cic.MutInd (u, t, exp_named_subst) ->
+ let l' = inspect_uri main l u [t] v term in
+ inspect_exp_named_subst l' (v+1) exp_named_subst
+ | Cic.MutConstruct (u, t, c, exp_named_subst) ->
+ let l' = inspect_uri main l u [t; c] v term in
+ inspect_exp_named_subst l' (v+1) exp_named_subst
| Cic.Cast (uu, _) ->
inspect_term main l v uu
| Cic.Prod (_, uu, tt) ->
let luu = inspect_term false l (v + 1) uu in
inspect_term false luu (v + 1) tt
| Cic.Appl m -> inspect_list main l true v m
- | Cic.MutCase (u, _, t, tt, uu, m) ->
+ | Cic.MutCase (u, t, tt, uu, m) ->
let lu = inspect_uri main l u [t] (v + 1) term in
let ltt = inspect_term false lu (v + 1) tt in
let luu = inspect_term false ltt (v + 1) uu in
| tt :: m ->
let ltt = inspect_term main l (if head then v else v + 1) tt in
inspect_list false ltt false v m
+ and inspect_exp_named_subst l v = function
+ [] -> l
+ | (_,t) :: tl ->
+ let l' = inspect_term false l v t in
+ inspect_exp_named_subst l' v tl
and inspect_ind l v = function
| [] -> l
| (_, _, tt, uu) :: m ->
let log q r =
let och = open_out_gen mode perm ! log_file in
if ! query_num = 1 then output_string och (time () ^ nl);
- let str = "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
- "Result:" ^ nl ^ Util.text_of_result r nl in
+ let str =
+ "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
+ "Result:" ^ nl ^ Util.text_of_result r nl in
output_string och str;
flush och
in
let locate s =
let module M = MathQL in
- let q = M.Ref (M.Fun "reference" (M.Const [s])) in
+ let q = M.Ref (M.Fun "nameObject" (M.Const [s])) in
execute_query q
-let backward e c t level =
+let searchPattern e c t level =
let module M = MathQL in
let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
let q_where = M.Sub (M.RefOf (
in
let build_select (r, b, v) =
let pos = if b then "MainConclusion" else "InConclusion" in
- M.Select ("uri",
- M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
- M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
- )
+ M.Select
+ ("uri",
+ M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
+ M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
+ )
in
let rec build_intersect = function
| [] -> M.Pattern (M.Const [".*"])
val locate : string -> MathQL.result
-val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result
+val searchPattern : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result
val get_query_info : unit -> string list
exception NotAnInductiveTypeToEliminate
exception NotTheRightEliminatorShape
exception NoHypothesesFound
+exception WrongUriToVariable of string
(* TODO problemone del fresh_name, aggiungerlo allo status? *)
let fresh_name () = "FOO"
match n with
C.Name _ -> n
(*CSC: generatore di nomi? Chiedere il nome? *)
- | C.Anonimous -> C.Name name
+ | C.Anonymous -> C.Name name
in
let (context',ty,bo) =
collect_context ((Some (n',(C.Decl s)))::context) t
function
t' when t' = S.lift n arg -> C.Rel (1 + n)
| C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
- | C.Var _
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
+ C.Var (uri,exp_named_subst')
| C.Meta _
| C.Sort _
| C.Implicit as t -> t
| C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
| C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
| C.Appl l -> C.Appl (List.map (aux n) l)
- | C.Const _ as t -> t
- | C.MutInd _
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,aux n outt, aux n t,
List.map (aux n) pl)
| C.Fix (i,fl) ->
let tylen = List.length fl in
fl
in
C.CoFix (i, substitutedfl)
+ and aux_exp_named_subst n =
+ List.map (function uri,t -> uri,aux n t)
in
let argty =
T.type_of_aux' metasenv context arg
(* a list of arguments for the new applications and the indexes of the first *)
(* and last new METAs introduced. The nth argument in the list of arguments *)
(* is just the nth new META. *)
-let new_metasenv_for_apply proof context ty =
+let new_metasenv_for_apply newmeta proof context ty =
let module C = Cic in
let module S = CicSubstitution in
let rec aux newmeta =
res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
| t -> t,[],[],newmeta
in
- let newmeta = new_meta ~proof in
- (* WARNING: here we are using the invariant that above the most *)
- (* recente new_meta() there are no used metas. *)
- let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
- res,newmetasenv,arguments,newmeta,lastmeta
+ (* WARNING: here we are using the invariant that above the most *)
+ (* recente new_meta() there are no used metas. *)
+ let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
+ res,newmetasenv,arguments,lastmeta
+
+(* Useful only inside apply_tac *)
+let
+ generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst
+=
+ let module C = Cic in
+ let params =
+ match CicEnvironment.get_obj uri with
+ C.Constant (_,_,_,params)
+ | C.CurrentProof (_,_,_,_,params)
+ | C.Variable (_,_,_,params)
+ | C.InductiveDefinition (_,params,_) -> params
+ in
+ let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
+ let next_fresh_meta = ref newmeta in
+ let newmetasenvfragment = ref [] in
+ let exp_named_subst_diff = ref [] in
+ let rec aux =
+ function
+ [],[] -> []
+ | uri::tl,[] ->
+ let ty =
+ match CicEnvironment.get_obj uri with
+ C.Variable (_,_,ty,_) ->
+ CicSubstitution.subst_vars !exp_named_subst_diff ty
+ | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ in
+ let irl = identity_relocation_list_for_metavariable context in
+ let subst_item = uri,C.Meta (!next_fresh_meta,irl) in
+ newmetasenvfragment :=
+ (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
+ exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
+ incr next_fresh_meta ;
+ subst_item::(aux (tl,[]))
+ | uri::tl1,((uri',_) as s)::tl2 ->
+ assert (UriManager.eq uri uri') ;
+ s::(aux (tl1,tl2))
+ | [],_ -> assert false
+ in
+ let exp_named_subst' = aux (params,exp_named_subst) in
+ !exp_named_subst_diff,!next_fresh_meta,
+ List.rev !newmetasenvfragment, exp_named_subst'
+ in
+prerr_endline ("@@@ " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst)) ^ " |--> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst'))) ;
+ new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
+;;
let apply_tac ~term ~status:(proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let termty = CicTypeChecker.type_of_aux' metasenv context term in
+ let newmeta = new_meta ~proof in
+ let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
+ match term with
+ C.Var (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Var (uri,exp_named_subst')
+ | C.Const (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | _ -> [],newmeta,[],term
+ in
+ let metasenv' = newmetasenvfragment@metasenv in
+prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ;
+ let termty =
+ CicSubstitution.subst_vars exp_named_subst_diff
+ (CicTypeChecker.type_of_aux' metasenv' context term)
+ in
+prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
(* newmeta is the lowest index of the new metas introduced *)
- let (consthead,newmetas,arguments,newmeta,_) =
- new_metasenv_for_apply proof context termty
+ let (consthead,newmetas,arguments,_) =
+ new_metasenv_for_apply newmeta' proof context termty
in
- let newmetasenv = newmetas@metasenv in
+ let newmetasenv = newmetas@metasenv' in
let subst,newmetasenv' =
CicUnification.fo_unif newmetasenv context consthead ty
in
let old_uninstantiatedmetas,new_uninstantiatedmetas =
(* subst_in doesn't need the context. Hence the underscore. *)
let subst_in _ = CicUnification.apply_subst subst in
- classify_metas newmeta in_subst_domain subst_in newmetasenv'
+ classify_metas newmeta' in_subst_domain subst_in newmetasenv'
in
let bo' =
- if List.length newmetas = 0 then
- term
- else
- let arguments' = List.map apply_subst arguments in
- Cic.Appl (term::arguments')
+ apply_subst
+ (if List.length newmetas = 0 then
+ term'
+ else
+ Cic.Appl (term'::arguments)
+ )
in
+prerr_endline ("XXXX " ^ CicPp.ppterm (if List.length newmetas = 0 then term' else Cic.Appl (term'::arguments)) ^ " |>>> " ^ CicPp.ppterm bo') ;
let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
let (newproof, newmetasenv''') =
let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in
let (curi,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let termty = T.type_of_aux' metasenv context term in
- let uri,cookingno,typeno,args =
+ let uri,exp_named_subst,typeno,args =
match termty with
- C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
- | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
- (uri,cookingno,typeno,args)
+ C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
| _ ->
prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty));
flush stderr;
let eliminator_uri =
let buri = U.buri_of_uri uri in
let name =
- match CicEnvironment.get_cooked_obj uri cookingno with
+ match CicEnvironment.get_obj uri with
C.InductiveDefinition (tys,_,_) ->
let (name,_,_,_) = List.nth tys typeno in
name
in
U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
in
- let eliminator_cookingno =
- UriManager.relative_depth curi eliminator_uri 0
- in
- let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
+(*CSC: BUG HERE!!! [] MUST BE COMPUTED SOMEHOW. USING UNIFICATION? *)
+ let eliminator_ref = C.Const (eliminator_uri,[]) in
let ety =
T.type_of_aux' [] [] eliminator_ref
in
let proof = ref (None : proof option)
let goal = ref (None : goal option)
-let apply_tactic ~tactic:tactic =
+let apply_or_can_apply_tactic ~try_only ~tactic =
match !proof,!goal with
None,_
| _,None -> assert false
| Some proof', Some goal' ->
let (newproof, newgoals) = tactic ~status:(proof', goal') in
- proof := Some newproof;
- goal :=
- (match newgoals, newproof with
- goal::_, _ -> Some goal
- | [], (_,(goal,_,_)::_,_,_) ->
+ if not try_only then
+ begin
+ proof := Some newproof;
+ goal :=
+ (match newgoals, newproof with
+ goal::_, _ -> Some goal
+ | [], (_,(goal,_,_)::_,_,_) ->
(* the tactic left no open goal ; let's choose the first open goal *)
(*CSC: here we could implement and use a proof-tree like notion... *)
- Some goal
- | _, _ -> None)
+ Some goal
+ | _, _ -> None)
+ end
+;;
+
+let apply_tactic = apply_or_can_apply_tactic ~try_only:false;;
+
+let can_apply_tactic ~tactic =
+ try
+ apply_or_can_apply_tactic ~try_only:true ~tactic ;
+ true
+ with
+ Fail _ -> false
+;;
(* metas_in_term term *)
(* Returns the ordered list of the metas that occur in [term]. *)
let module C = Cic in
let rec aux =
function
- C.Rel _
- | C.Var _ -> []
+ C.Rel _ -> []
| C.Meta (n,_) -> [n]
| C.Sort _
| C.Implicit -> []
| C.Lambda (_,s,t) -> (aux s) @ (aux t)
| C.LetIn (_,s,t) -> (aux s) @ (aux t)
| C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
- | C.Const _
- | C.MutInd _
- | C.MutConstruct _ -> []
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ | C.Var (_,exp_named_subst)
+ | C.Const (_,exp_named_subst)
+ | C.MutInd (_,_,exp_named_subst)
+ | C.MutConstruct (_,_,_,exp_named_subst) ->
+ List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst
+ | C.MutCase (_,_,outt,t,pl) ->
(aux outt) @ (aux t) @
(List.fold_left (fun i t -> i @ (aux t)) [] pl)
- | C.Fix (i,fl) ->
+ | C.Fix (_,fl) ->
List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
- | C.CoFix (i,fl) ->
+ | C.CoFix (_,fl) ->
List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
in
let metas = aux term in
(*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
(*CSC: che si guadagni nulla in fatto di efficienza. *)
let replace =
- ProofEngineReduction.replace
- ~equality:
- (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
- ~what:term' ~with_what:term
+ ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term
in
let ty' = replace ty in
let context' =
(* primitive tactics *)
+let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
let intros () =
apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term
(* "primitive" tactics *)
+val can_apply : Cic.term -> bool
val apply : Cic.term -> unit
val intros : unit -> unit
val cut : Cic.term -> unit
(* The code of this module is derived from the code of CicReduction *)
exception Impossible of int;;
-exception ReferenceToDefinition;;
-exception ReferenceToAxiom;;
+exception ReferenceToConstant;;
exception ReferenceToVariable;;
exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
exception WrongUriToInductiveDefinition;;
exception RelToHiddenHypothesis;;
-(* syntactic_equality up to cookingsno for uris *)
-(* (which is often syntactically irrilevant) *)
-let syntactic_equality ~alpha_equivalence =
+let alpha_equivalence =
let module C = Cic in
let rec aux t t' =
if t = t' then true
else
match t,t' with
- C.Rel _, C.Rel _
- | C.Var _, C.Var _
- | C.Meta _, C.Meta _
- | C.Sort _, C.Sort _
- | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+ C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2) ->
+ UriManager.eq uri1 uri2 &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
| C.Cast (te,ty), C.Cast (te',ty') ->
aux te te' && aux ty ty'
- | C.Prod (n,s,t), C.Prod (n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
- | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
- | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
- (alpha_equivalence || n = n') && aux s s' && aux t t'
+ | C.Prod (_,s,t), C.Prod (_,s',t') ->
+ aux s s' && aux t t'
+ | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
+ aux s s' && aux t t'
+ | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
+ aux s s' && aux t t'
| C.Appl l, C.Appl l' ->
(try
List.fold_left2
(fun b t1 t2 -> b && aux t1 t2) true l l'
with
Invalid_argument _ -> false)
- | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
- | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
- UriManager.eq uri uri' && i = i'
- | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
- UriManager.eq uri uri' && i = i' && j = j'
- | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+ | C.Const (uri,exp_named_subst1), C.Const (uri',exp_named_subst2) ->
+ UriManager.eq uri uri' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutInd (uri,i,exp_named_subst1), C.MutInd (uri',i',exp_named_subst2) ->
+ UriManager.eq uri uri' && i = i' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutConstruct (uri,i,j,exp_named_subst1),
+ C.MutConstruct (uri',i',j',exp_named_subst2) ->
+ UriManager.eq uri uri' && i = i' && j = j' &&
+ aux_exp_named_subst exp_named_subst1 exp_named_subst2
+ | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
UriManager.eq sp sp' && i = i' &&
aux outt outt' && aux t t' &&
(try
i = i' &&
(try
List.fold_left2
- (fun b (name,i,ty,bo) (name',i',ty',bo') ->
- b && (alpha_equivalence || name = name') && i = i' &&
- aux ty ty' && aux bo bo') true fl fl'
+ (fun b (_,i,ty,bo) (_,i',ty',bo') ->
+ b && i = i' && aux ty ty' && aux bo bo'
+ ) true fl fl'
with
Invalid_argument _ -> false)
| C.CoFix (i,fl), C.CoFix (i',fl') ->
i = i' &&
(try
List.fold_left2
- (fun b (name,ty,bo) (name',ty',bo') ->
- b && (alpha_equivalence || name = name') &&
- aux ty ty' && aux bo bo') true fl fl'
+ (fun b (_,ty,bo) (_,ty',bo') ->
+ b && aux ty ty' && aux bo bo'
+ ) true fl fl'
with
Invalid_argument _ -> false)
- | _,_ -> false
- in
- aux
+ | _,_ -> false (* we already know that t != t' *)
+ and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
+ try
+ List.fold_left2
+ (fun b (uri1,t1) (uri2,t2) ->
+ b && UriManager.eq uri1 uri2 && aux t1 t2
+ ) true exp_named_subst1 exp_named_subst2
+ with
+ Invalid_argument _ -> false
+ in
+ aux
;;
(* "textual" replacement of a subterm with another one *)
function
t when (equality t what) -> with_what
| C.Rel _ as t -> t
- | C.Var _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
| C.Meta _ as t -> t
| C.Sort _ as t -> t
| C.Implicit as t -> t
(match List.map aux l with
(C.Appl l')::tl -> C.Appl (l'@tl)
| l' -> C.Appl 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 outt, aux t,
- List.map aux pl)
+ | C.Const (uri,exp_named_subst) ->
+ C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutInd (uri,i,exp_named_subst) ->
+ C.MutInd
+ (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ C.MutConstruct
+ (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,aux outt, aux t,List.map aux pl)
| C.Fix (i,fl) ->
let substitutedfl =
List.map
function
t when (equality t what) -> S.lift (k-1) with_what
| C.Rel n as t -> t
- | C.Var _ as t -> t
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what 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 what outt, substaux k what t,
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k what outt, substaux k what t,
List.map (substaux k what) pl)
| C.Fix (i,fl) ->
let len = List.length fl in
| Some (_,C.Def bo) -> reduceaux context 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) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_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,_) -> reduceaux context l body
+ | C.Variable (_,None,_,_) ->
+ let t' = C.Var (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.Variable (_,Some body,_,_) ->
+ (reduceaux context 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 *)
let tl' = List.map (reduceaux context []) tl in
reduceaux context (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,_,_) -> reduceaux context l body
- | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
- | C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduceaux context l 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,outtype,term,pl) ->
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ (reduceaux context l
+ (CicSubstitution.subst_vars exp_named_subst' body))
+ | C.Constant (_,None,_,_) ->
+ let t' = C.Const (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.Variable _ -> raise ReferenceToVariable
+ | C.CurrentProof (_,_,body,_,_) ->
+ (reduceaux context l
+ (CicSubstitution.subst_vars exp_named_subst' body))
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ )
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutInd (uri,i,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
| t -> t
in
(match decofix (reduceaux context [] term) with
- C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
- | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
- let (arity, r, num_ingredients) =
+ C.MutConstruct (_,_,j,_) -> reduceaux context 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)
+ C.InductiveDefinition (tl,_,r) ->
+ 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
reduceaux context (ts@l) (List.nth pl (j-1))
| C.Cast _ | C.Implicit ->
let term' = reduceaux context [] term in
let pl' = List.map (reduceaux context []) pl in
let res =
- C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ C.MutCase (mutind,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
C.CoFix (i, fl')
in
if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+ List.map (function uri,t -> uri,reduceaux context l t)
in
reduceaux context []
;;
| Some (_,C.Def bo) -> reduceaux context 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.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
- | C.Variable (_,Some body,_) -> reduceaux context l body
- )
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant _ -> raise ReferenceToConstant
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_,_) ->
+ let t' = C.Var (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.Variable (_,Some body,_,_) ->
+ reduceaux context 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.Implicit as t -> t
let tl' = List.map (reduceaux context []) tl in
reduceaux context (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,_,_) ->
- begin
- try
- (**** Step 2 ****)
- let res,constant_args =
- let rec aux rev_constant_args l =
- function
- C.Lambda (name,s,t) as t' ->
- begin
- match l with
- [] -> raise WrongShape
- | he::tl ->
- (* when name is Anonimous the substitution should be *)
- (* superfluous *)
- aux (he::rev_constant_args) tl (S.subst he t)
- end
- | C.LetIn (_,s,t) ->
- aux rev_constant_args l (S.subst s t)
- | C.Fix (i,fl) as t ->
- let tys =
- List.map (function (name,_,ty,_) ->
- Some (C.Name name, C.Decl ty)) fl
- in
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- List.nth l recindex
- with
- _ -> raise AlreadySimplified
- in
- (match CicReduction.whd context recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (function _ ->
- decr counter ; S.subst (C.Fix (!counter,fl))
- ) fl body
- in
- (* Possible optimization: substituting whd *)
- (* recparam in l *)
- reduceaux (tys@context) l body',
- List.rev rev_constant_args
- | _ -> raise AlreadySimplified
- )
- | _ -> raise WrongShape
- in
- aux [] l body
- in
- (**** Step 3 ****)
- let term_to_fold =
- match constant_args with
- [] -> C.Const (uri,cookingsno)
- | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ begin
+ try
+ (**** Step 2 ****)
+ let res,constant_args =
+ let rec aux rev_constant_args l =
+ function
+ C.Lambda (name,s,t) as t' ->
+ begin
+ match l with
+ [] -> raise WrongShape
+ | he::tl ->
+ (* when name is Anonimous the substitution should *)
+ (* be superfluous *)
+ aux (he::rev_constant_args) tl (S.subst he t)
+ end
+ | C.LetIn (_,s,t) ->
+ aux rev_constant_args l (S.subst s t)
+ | C.Fix (i,fl) as t ->
+ let tys =
+ List.map (function (name,_,ty,_) ->
+ Some (C.Name name, C.Decl ty)) fl
+ in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ List.nth l recindex
+ with
+ _ -> raise AlreadySimplified
+ in
+ (match CicReduction.whd context recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (function _ ->
+ decr counter ; S.subst (C.Fix (!counter,fl))
+ ) fl body
+ in
+ (* Possible optimization: substituting whd *)
+ (* recparam in l *)
+ reduceaux (tys@context) l body',
+ List.rev rev_constant_args
+ | _ -> raise AlreadySimplified
+ )
+ | _ -> raise WrongShape
+ in
+ aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
in
- let reduced_term_to_fold = reduce context term_to_fold in
- replace (=) reduced_term_to_fold term_to_fold res
- with
- WrongShape ->
- (* The constant does not unfold to a Fix lambda-abstracted *)
- (* w.r.t. zero or more variables. We just perform reduction. *)
- reduceaux context l body
- | AlreadySimplified ->
- (* If we performed delta-reduction, we would find a Fix *)
- (* not applied to a constructor. So, we refuse to perform *)
- (* delta-reduction. *)
- if l = [] then
- t
- else
- C.Appl (t::l)
- end
- | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
+ (**** Step 3 ****)
+ let term_to_fold =
+ match constant_args with
+ [] -> C.Const (uri,exp_named_subst')
+ | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args)
+ in
+ let reduced_term_to_fold = reduce context term_to_fold in
+ replace (=) reduced_term_to_fold term_to_fold res
+ with
+ WrongShape ->
+ (* The constant does not unfold to a Fix lambda-abstracted *)
+ (* w.r.t. zero or more variables. We just perform reduction.*)
+ reduceaux context l
+ (CicSubstitution.subst_vars exp_named_subst' body)
+ | AlreadySimplified ->
+ (* If we performed delta-reduction, we would find a Fix *)
+ (* not applied to a constructor. So, we refuse to perform *)
+ (* delta-reduction. *)
+ let t' = C.Const (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ end
+ | C.Constant (_,None,_,_) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.Const (uri,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_) -> reduceaux context l body
+ | C.CurrentProof (_,_,body,_,_) -> reduceaux context l 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,outtype,term,pl) ->
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutInd (uri,i,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ let t' = C.MutConstruct(uri,i,j,exp_named_subst') in
+ if l = [] then t' else C.Appl (t'::l)
+ | C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
C.CoFix (i,fl) as t ->
| t -> t
in
(match decofix (reduceaux context [] term) with
- C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
- | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
- let (arity, r, num_ingredients) =
+ C.MutConstruct (_,_,j,_) -> reduceaux context 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
reduceaux context (ts@l) (List.nth pl (j-1))
| C.Cast _ | C.Implicit ->
let term' = reduceaux context [] term in
let pl' = List.map (reduceaux context []) pl in
let res =
- C.MutCase (mutind,cookingsno,i,outtype',term',pl')
+ C.MutCase (mutind,i,outtype',term',pl')
in
if l = [] then res else C.Appl (res::l)
)
C.CoFix (i, fl')
in
if l = [] then t' else C.Appl (t'::l)
+ and reduceaux_exp_named_subst context l =
+ List.map (function uri,t -> uri,reduceaux context l t)
in
reduceaux context []
;;
*)
exception Impossible of int
-exception ReferenceToDefinition
-exception ReferenceToAxiom
+exception ReferenceToConstant
exception ReferenceToVariable
exception ReferenceToCurrentProof
exception ReferenceToInductiveDefinition
exception WrongShape
exception AlreadySimplified
-val syntactic_equality : alpha_equivalence:bool -> Cic.term -> Cic.term -> bool
+val alpha_equivalence: Cic.term -> Cic.term -> bool
val replace :
equality:(Cic.term -> 'a -> bool) ->
what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
let string_of_name =
function
C.Name n -> n
- | C.Anonimous -> "_"
+ | C.Anonymous -> "_"
in
let metasenv' =
List.map
let string_of_name =
function
C.Name n -> n
- | C.Anonimous -> "_"
+ | C.Anonymous -> "_"
in
let metasenv' =
List.map
+(* Copyright (C) 2002, 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/.
+ *)
+
val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"
let refl_eqt_uri = (eqt_uri, 0, 1)
-let sym_eqt_uri =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con"
+let equality_is_a_congruence_A =
+ uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+let equality_is_a_congruence_x =
+ uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+let equality_is_a_congruence_y =
+ uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
+let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con"
let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind"
let true_uri = (bool_uri, 0, 1)
let false_uri = (bool_uri, 0, 2)
let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con"
let apolynomial_uri =
- uri_of_string
- "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind"
+ uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
let apvar_uri = (apolynomial_uri, 0, 1)
let ap0_uri = (apolynomial_uri, 0, 2)
let ap1_uri = (apolynomial_uri, 0, 3)
let apmult_uri = (apolynomial_uri, 0, 5)
let apopp_uri = (apolynomial_uri, 0, 6)
-let varmap_uri =
- uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap.ind"
+let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
+let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
let empty_vm_uri = (varmap_uri, 0, 1)
let node_vm_uri = (varmap_uri, 0, 2)
-let varmap_find_uri =
- uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap_find.con"
-let index_uri =
- uri_of_string "cic:/Coq/ring/Quote/variables_map/index.ind"
+let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
+let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
let left_idx_uri = (index_uri, 0, 1)
let right_idx_uri = (index_uri, 0, 2)
let end_idx_uri = (index_uri, 0, 3)
-let interp_ap_uri =
- uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con"
+let abstract_rings_A_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
+let abstract_rings_Aplus_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
+let abstract_rings_Amult_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
+let abstract_rings_Aone_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
+let abstract_rings_Azero_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
+let abstract_rings_Aopp_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
+let abstract_rings_Aeq_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
+let abstract_rings_vm_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
+let abstract_rings_T_uri =
+ uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
+let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
let interp_sacs_uri =
- uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con"
+ uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
let apolynomial_normalize_uri =
- uri_of_string
- "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con"
+ uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
let apolynomial_normalize_ok_uri =
- uri_of_string
- "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con"
+ uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"
(** CIC PREDICATES *)
Create a Cic term consisting of a constant
@param uri URI of the constant
@proof current proof
+ @exp_named_subst explicit named substitution
*)
-let mkConst ~uri ~proof =
- let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
- Cic.Const (uri, cookingsno)
+let mkConst ~uri ~exp_named_subst =
+ Cic.Const (uri, exp_named_subst)
(**
Create a Cic term consisting of a constructor
@param uri triple <uri, typeno, consno> where uri is the uri of an inductive
type, typeno is the type number in a mutind structure (0 based), consno is
the constructor number (1 based)
- @param proof current proof
+ @exp_named_subst explicit named substitution
*)
-let mkCtor ~uri:(uri, typeno, consno) ~proof =
- let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
- Cic.MutConstruct (uri, cookingsno, typeno, consno)
+let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
+ Cic.MutConstruct (uri, typeno, consno, exp_named_subst)
(**
Create a Cic term consisting of a type member of a mutual induction
@param uri pair <uri, typeno> where uri is the uri of a mutual inductive
type and typeno is the type number (0 based) in the mutual induction
+ @exp_named_subst explicit named substitution
*)
-let mkMutInd ~uri:(uri, typeno) ~proof =
- let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in
- Cic.MutInd (uri, cookingsno, typeno)
+let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
+ Cic.MutInd (uri, typeno, exp_named_subst)
(** EXCEPTIONS *)
(**
Check whether the ring tactic can be applied on a given term (i.e. that is
an equality on reals)
- @param term term to be tested
+ @param term to be tested
@return true if the term is ringable, false otherwise
*)
let ringable =
let is_equality = function
- | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true
+ | Cic.MutInd uri 0 [] when (eq uri eqt_uri) -> true
| _ -> false
in
let is_real = function
@return an index representing the same node in a varmap (@see varmap_uri),
the returned index is as defined in index (@see index_uri)
*)
-let path_of_int n proof =
+let path_of_int n =
let rec digits_of_int n =
if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
in
List.fold_right
(fun digit path ->
Cic.Appl [
- mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof;
+ mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
path])
(List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
- (mkCtor end_idx_uri proof)
+ (mkCtor end_idx_uri [])
(**
Build a variable map (@see varmap_uri) from a variables array.
/ \
y z
@param vars variables array
- @param proof current proof
@return a cic term representing the variable map containing vars variables
*)
-let btree_of_array ~vars ~proof =
- let r = mkConst r_uri proof in (* cic objects *)
- let empty_vm = mkCtor empty_vm_uri proof in
- let empty_vm_r = Cic.Appl [empty_vm; r] in
- let node_vm = mkCtor node_vm_uri proof in
- let node_vm_r = Cic.Appl [node_vm; r] in
+let btree_of_array ~vars =
+ let r = mkConst r_uri [] in (* cic objects *)
+ let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
+ let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
let size = Array.length vars in
let halfsize = size lsr 1 in
let rec aux n = (* build the btree starting from position n *)
if n > size then
empty_vm_r
else if n > halfsize then (* no more children *)
- Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r]
+ Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
else (* still children *)
- Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)]
+ Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
in
aux 1
abstraction function:
concrete polynoms -----> (abstract polynoms, varmap)
@param terms list of conrete polynoms
- @param proof current proof
@return a pair <aterms, varmap> where aterms is a list of abstract polynoms
and varmap is the variable map needed to interpret them
*)
-let abstract_poly ~terms ~proof =
+let abstract_poly ~terms =
let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
let varlist = ref [] in (* vars list in reverse order *)
let counter = ref 1 in (* index of next new variable *)
(* "bop" -> binary operator | "uop" -> unary operator *)
| Cic.Appl (bop::t1::t2::[])
when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *)
- Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2]
+ Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
| Cic.Appl (bop::t1::t2::[])
when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *)
- Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2]
+ Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
| Cic.Appl (uop::t::[])
when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *)
- Cic.Appl [mkCtor apopp_uri proof; aux t]
+ Cic.Appl [mkCtor apopp_uri []; aux t]
| t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *)
- mkCtor ap0_uri proof
+ mkCtor ap0_uri []
| t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *)
- mkCtor ap1_uri proof
+ mkCtor ap1_uri []
| t -> (* variable *)
try
Hashtbl.find varhash t (* use an old var *)
with Not_found -> begin (* create a new var *)
let newvar =
- Cic.Appl [mkCtor apvar_uri proof; path_of_int !counter proof]
+ Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
in
incr counter;
varlist := t :: !varlist;
in
let aterms = List.map aux terms in (* abstract vars *)
let varmap = (* build varmap *)
- btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof
+ btree_of_array ~vars:(Array.of_list (List.rev !varlist))
in
(aterms, varmap)
t''' = apolynomial_normalize_ok(varmap, at)
at is the abstract term built from t, t is a single member of aterms
*)
-let build_segments ~terms ~proof =
- let r = mkConst r_uri proof in (* cic objects *)
- let rplus = mkConst rplus_uri proof in
- let rmult = mkConst rmult_uri proof in
- let ropp = mkConst ropp_uri proof in
- let r0 = mkConst r0_uri proof in
- let r1 = mkConst r1_uri proof in
- let interp_ap = mkConst interp_ap_uri proof in
- let interp_sacs = mkConst interp_sacs_uri proof in
- let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in
- let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in
- let rtheory = mkConst rtheory_uri proof in
+let build_segments ~terms =
+ let r = mkConst r_uri [] in (* cic objects *)
+ let rplus = mkConst rplus_uri [] in
+ let rmult = mkConst rmult_uri [] in
+ let ropp = mkConst ropp_uri [] in
+ let r1 = mkConst r1_uri [] in
+ let r0 = mkConst r0_uri [] in
+ let theory_args_subst varmap =
+ [abstract_rings_A_uri, r ;
+ abstract_rings_Aplus_uri, rplus ;
+ abstract_rings_Amult_uri, rmult ;
+ abstract_rings_Aone_uri, r1 ;
+ abstract_rings_Azero_uri, r0 ;
+ abstract_rings_Aopp_uri, ropp ;
+ abstract_rings_vm_uri, varmap] in
+ let theory_args_subst' eq varmap t =
+ [abstract_rings_A_uri, r ;
+ abstract_rings_Aplus_uri, rplus ;
+ abstract_rings_Amult_uri, rmult ;
+ abstract_rings_Aone_uri, r1 ;
+ abstract_rings_Azero_uri, r0 ;
+ abstract_rings_Aopp_uri, ropp ;
+ abstract_rings_Aeq_uri, eq ;
+ abstract_rings_vm_uri, varmap ;
+ abstract_rings_T_uri, t] in
+ let interp_ap varmap =
+ mkConst interp_ap_uri (theory_args_subst varmap) in
+ let interp_sacs varmap =
+ mkConst interp_sacs_uri (theory_args_subst varmap) in
+ let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
+ let apolynomial_normalize_ok eq varmap t =
+ mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
+ let rtheory = mkConst rtheory_uri [] in
let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
- Cic.Lambda (Cic.Anonimous, r,
- Cic.Lambda (Cic.Anonimous, r,
- mkCtor false_uri proof))
+ Cic.Lambda (Cic.Anonymous, r,
+ Cic.Lambda (Cic.Anonymous, r,
+ mkCtor false_uri []))
in
- let theory_args = [r; rplus; rmult; r1; r0; ropp] in
- let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *)
+ let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
List.map (* build ring segments *)
- (fun t ->
- Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]),
- Cic.Appl (
- interp_sacs ::
- (theory_args @
- [varmap; Cic.Appl [apolynomial_normalize; t]])),
- Cic.Appl (
- (apolynomial_normalize_ok :: theory_args) @
- [lxy_false; varmap; rtheory; t]))
- aterms
+ (fun t ->
+ Cic.Appl [interp_ap varmap ; t],
+ Cic.Appl (
+ [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
+ Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t]
+ ) aterms
let id_tac ~status:(proof,goal) =
(proof,[goal])
*)
let reflexivity_tac ~status:(proof, goal) =
warn "in Ring.reflexivity_tac";
- let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in
+ let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
try
apply_tac ~status:(proof, goal) ~term:refl_eqt
with (Fail _) as e ->
Ring tactic, does associative and commutative rewritings in Reals ring
@param status current proof engine status
*)
-let ring_tac ~status:(proof, goal) =
+let ring_tac ~status:((proof, goal) as status) =
warn "in Ring tactic";
- let status = (proof, goal) in
- let eqt = mkMutInd (eqt_uri, 0) proof in
- let r = mkConst r_uri proof in
+ let eqt = mkMutInd (eqt_uri, 0) [] in
+ let r = mkConst r_uri [] in
let metasenv = metasenv_of_status ~status in
let (metano, context, ty) = conj_of_metano goal metasenv in
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
- match (build_segments ~terms:[t1; t2] ~proof) with
+ match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
List.iter (* debugging, feel free to remove *)
(fun (descr, term) ->
Tacticals.try_tactics
~status
~tactics:[
- "reflexivity", reflexivity_tac;
- "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'';
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
- "exact sym_eqt su t1 ...", exact_tac ~term:(
- Cic.Appl [
- mkConst sym_eqt_uri proof; mkConst r_uri proof;
- t1''; t1; t1'_eq_t1'']);
+ "reflexivity", reflexivity_tac ;
+ "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
+ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
+ "exact sym_eqt su t1 ...", exact_tac
+ ~term:(
+ Cic.Appl
+ [mkConst sym_eqt_uri
+ [equality_is_a_congruence_A, mkConst r_uri [] ;
+ equality_is_a_congruence_x, t1'' ;
+ equality_is_a_congruence_y, t1
+ ] ;
+ t1'_eq_t1''
+ ]) ;
"elim_type eqt su t1 ...", (fun ~status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status ~status in
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",
- exact_tac ~term:(
- Cic.Appl [
- mkConst sym_eqt_uri proof;
- mkConst r_uri proof;
- t2''; t2; t2'_eq_t2'']);
+ exact_tac
+ ~term:(
+ Cic.Appl
+ [mkConst sym_eqt_uri
+ [equality_is_a_congruence_A, mkConst r_uri [] ;
+ equality_is_a_congruence_x, t2'' ;
+ equality_is_a_congruence_y, t2
+ ] ;
+ t2'_eq_t2''
+ ]) ;
"elim_type eqt su t2 ...", (fun ~status ->
let status' =
let context = context_of_status ~status in
let print_name =
function
Cic.Name n -> n
- | Cic.Anonimous -> "_"
+ | Cic.Anonymous -> "_"
in
List.fold_right
(fun i (output,context) ->
module XmlPp =
struct
+ let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";;
+
let print_sequent metasenv (metano,context,goal) =
let module X = Xml in
let ids_to_terms = Hashtbl.create 503 in
let ids_to_inner_types = Hashtbl.create 503 in
let ids_to_hypotheses = Hashtbl.create 11 in
let hypotheses_seed = ref 0 in
- let seed = ref 0 in
+ let sequent_id = "i0" in
+ let seed = ref 1 in (* 'i0' is used for the whole sequent *)
let acic_of_cic_context =
Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids
ids_to_inner_sorts ids_to_inner_types metasenv
in
- let final_s,_ =
+ let final_s,_,final_idrefs =
(List.fold_right
- (fun binding (s,context) ->
+ (fun binding (s,context,idrefs) ->
let hid = "h" ^ string_of_int !hypotheses_seed in
Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
(Some (n,(Cic.Def t as b)) as entry)
| (Some (n,(Cic.Decl t as b)) as entry) ->
- let acic = acic_of_cic_context context t None in
+ let acic = acic_of_cic_context context idrefs t None in
[< s ;
X.xml_nempty
(match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
["name",(match n with Cic.Name n -> n | _ -> assert false);
"id",hid]
- (Cic2Xml.print_term
- (UriManager.uri_of_string "cic:/dummy.con")
- ~ids_to_inner_sorts acic)
- >], (entry::context)
+ (Cic2Xml.print_term ~ids_to_inner_sorts acic)
+ >], (entry::context), (hid::idrefs)
| None ->
- [< s ; X.xml_empty "Hidden" [] >], (None::context)
- ) context ([<>],[])
+ (* Invariant: "" is never looked up *)
+ [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+ ) context ([<>],[],[])
)
in
- let acic = acic_of_cic_context context goal None in
- X.xml_nempty "Sequent" ["no",string_of_int metano]
- [< final_s ;
- Xml.xml_nempty "Goal" []
- (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
- ~ids_to_inner_sorts acic)
+ let acic = acic_of_cic_context context final_idrefs goal None in
+ [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\n");
+ X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id]
+ [< final_s ;
+ Xml.xml_nempty "Goal" []
+ (Cic2Xml.print_term ~ids_to_inner_sorts acic)
+ >]
>],
ids_to_terms,ids_to_father_ids,ids_to_hypotheses
;;
(** DEBUGGING *)
(** perform debugging output? *)
-let debug = false
+let debug = true
(** debugging print *)
let warn s =
let pp_type_of uri =
let u = UriManager.uri_of_string uri in
let s = match (CicEnvironment.get_obj u) with
- | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
- | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty
- | Cic.Variable (_, _, ty) -> CicPp.ppterm ty
- | _ -> "Current proof or inductive definition."
+ | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
+ | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
+ | _ -> "Current proof or inductive definition."
(*
| Cic.CurrentProof (_,conjs,te,ty) ->
| C.InductiveDefinition _ ->
let module G = Gdome in
let module X = Xml in
let root_name,root_attributes,root_content =
+ ignore (Stream.next strm) ; (* to skip the <?xml ...?> declaration *)
+ ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *)
match Stream.next strm with
X.Empty(n,l) -> n,l,[<>]
| X.NEmpty(n,l,c) -> n,l,c
projects / helm.git / commitdiff