From: Claudio Sacerdoti Coen Date: Wed, 30 Oct 2002 15:04:44 +0000 (+0000) Subject: - (Partial) porting to the new theory with explicit named substitutions X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7074f0403d1bec7f4d60715e50a0fe0ef0993567;p=helm.git - (Partial) porting to the new theory with explicit named substitutions - Porting to the new DTD - Porting to the new query language and to its implementation - searchPattern implemented: it performs an old "backward" query and then tries to apply every result to filter out false matches Open bugs: - ElimIntrosSimpl, Fourier and Ring still to be ported - many, many, many others --- diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index 7c674d0ad..fa7d729d9 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -27,27 +27,30 @@ 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] @@ -68,65 +71,113 @@ let print_term curi ~ids_to_inner_sorts = 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) ; @@ -143,9 +194,9 @@ let print_term curi ~ids_to_inner_sorts = 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 >] >] ; @@ -158,8 +209,8 @@ let print_term curi ~ids_to_inner_sorts = 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 >] >] ; @@ -167,67 +218,129 @@ let print_term curi ~ids_to_inner_sorts = >] ) 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 "\n" ; + X.xml_cdata ("\n"); + xml_for_current_proof_body + >] in + let xmlty = + [< X.xml_cdata "\n" ; + X.xml_cdata + ("\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 + "\n" ; + X.xml_cdata + ("\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 "\n" ; + X.xml_cdata ("\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 @@ -241,10 +354,10 @@ let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types = (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 [<>] diff --git a/helm/gTopLevel/cic2Xml.mli b/helm/gTopLevel/cic2Xml.mli index 62a423f58..52a6f77eb 100644 --- a/helm/gTopLevel/cic2Xml.mli +++ b/helm/gTopLevel/cic2Xml.mli @@ -27,14 +27,13 @@ exception ImpossiblePossible 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 -> diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml index f08bb877a..8d849634d 100644 --- a/helm/gTopLevel/cic2acic.ml +++ b/helm/gTopLevel/cic2acic.ml @@ -29,10 +29,15 @@ type anntypes = {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 @@ -52,7 +57,7 @@ let rec get_nth l n = ;; 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 @@ -61,7 +66,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -100,11 +105,13 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -127,12 +134,16 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -145,7 +156,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts (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) @@ -154,13 +165,13 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -177,38 +188,54 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -216,12 +243,16 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 @@ -229,23 +260,24 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts 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 ;; @@ -263,54 +295,68 @@ let acic_object_of_cic_object obj = 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, diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli index a07b9d297..bc174d121 100644 --- a/helm/gTopLevel/cic2acic.mli +++ b/helm/gTopLevel/cic2acic.mli @@ -39,6 +39,7 @@ val acic_of_cic_context' : (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 *) diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml index b06619c4d..4afe0e475 100644 --- a/helm/gTopLevel/doubleTypeInference.ml +++ b/helm/gTopLevel/doubleTypeInference.ml @@ -39,8 +39,12 @@ let rec head_beta_reduce = 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 @@ -64,11 +68,23 @@ let rec head_beta_reduce = 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' = @@ -99,11 +115,9 @@ let syntactic_equality 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 (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' @@ -118,12 +132,17 @@ let syntactic_equality t t' = 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' && @@ -143,7 +162,11 @@ let 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' @@ -158,20 +181,19 @@ let rec split l n = | (_,_) -> 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)) ;; @@ -179,20 +201,19 @@ let type_of_variable 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") @@ -204,12 +225,12 @@ let cooked_type_of_mutual_inductive_defs uri cookingsno i = | _ -> 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") @@ -217,7 +238,7 @@ let cooked_type_of_mutual_inductive_constr uri cookingsno i j = match cobj with C.InductiveDefinition (dl,_,_) -> let (_,_,_,cl) = List.nth dl i in - let (_,ty,_) = List.nth cl (j-1) in + let (_,ty) = List.nth cl (j-1) in ty | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) ;; @@ -253,7 +274,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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,_) = @@ -355,14 +378,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 = @@ -373,10 +400,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -386,7 +412,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -395,18 +421,20 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = (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) | _ -> @@ -414,12 +442,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -502,6 +530,34 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty = 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 @@ -551,7 +607,7 @@ and type_of_branch context argsno need_dummy outtype term constype = C.Appl l -> C.Appl (l@[C.Rel 1]) | t -> C.Appl [t ; C.Rel 1] in - C.Prod (C.Anonimous,so,type_of_branch + C.Prod (C.Anonymous,so,type_of_branch ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) | _ -> raise (Impossible 20) diff --git a/helm/gTopLevel/esempi/and_implies_or2.cic b/helm/gTopLevel/esempi/and_implies_or2.cic index f693df30c..46cfb9e1b 100644 --- a/helm/gTopLevel/esempi/and_implies_or2.cic +++ b/helm/gTopLevel/esempi/and_implies_or2.cic @@ -1,8 +1,8 @@ -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) diff --git a/helm/gTopLevel/esempi/apply.cic b/helm/gTopLevel/esempi/apply.cic index fb27e1693..902ae2fbb 100644 --- a/helm/gTopLevel/esempi/apply.cic +++ b/helm/gTopLevel/esempi/apply.cic @@ -1,6 +1,6 @@ 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 @@ -10,7 +10,7 @@ alias lt /Coq/Init/Peano/lt.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)) diff --git a/helm/gTopLevel/esempi/bug.cic b/helm/gTopLevel/esempi/bug.cic index 2f10c572c..cab0f5ff2 100644 --- a/helm/gTopLevel/esempi/bug.cic +++ b/helm/gTopLevel/esempi/bug.cic @@ -1,9 +1,9 @@ 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 @@ -11,12 +11,12 @@ alias mult /Coq/Init/Peano/mult.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) diff --git a/helm/gTopLevel/esempi/calcolo_proposizioni.cic b/helm/gTopLevel/esempi/calcolo_proposizioni.cic index 5fe90ed32..a069a8b39 100644 --- a/helm/gTopLevel/esempi/calcolo_proposizioni.cic +++ b/helm/gTopLevel/esempi/calcolo_proposizioni.cic @@ -5,13 +5,13 @@ alias True_ind /Coq/Init/Logic/True_ind.con 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 diff --git a/helm/gTopLevel/esempi/conversion.cic b/helm/gTopLevel/esempi/conversion.cic index 3964f6f12..9114f3aa5 100644 --- a/helm/gTopLevel/esempi/conversion.cic +++ b/helm/gTopLevel/esempi/conversion.cic @@ -1,9 +1,9 @@ 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 @@ -11,7 +11,7 @@ alias mult /Coq/Init/Peano/mult.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)) diff --git a/helm/gTopLevel/esempi/elim.cic b/helm/gTopLevel/esempi/elim.cic index eb679d686..0ef611ff7 100644 --- a/helm/gTopLevel/esempi/elim.cic +++ b/helm/gTopLevel/esempi/elim.cic @@ -1,6 +1,6 @@ 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 @@ -8,6 +8,6 @@ alias mult /Coq/Init/Peano/mult.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)) diff --git a/helm/gTopLevel/esempi/evars.cic b/helm/gTopLevel/esempi/evars.cic index 9183cb1e4..36ce17e2e 100644 --- a/helm/gTopLevel/esempi/evars.cic +++ b/helm/gTopLevel/esempi/evars.cic @@ -1,9 +1,9 @@ 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 @@ -11,7 +11,7 @@ alias mult /Coq/Init/Peano/mult.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 diff --git a/helm/gTopLevel/esempi/prova.cic b/helm/gTopLevel/esempi/prova.cic index 6ca06a862..3f65458d2 100644 --- a/helm/gTopLevel/esempi/prova.cic +++ b/helm/gTopLevel/esempi/prova.cic @@ -1,4 +1,4 @@ -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 diff --git a/helm/gTopLevel/esempi/sets.cic b/helm/gTopLevel/esempi/sets.cic index 156e231a2..5bd913e72 100644 --- a/helm/gTopLevel/esempi/sets.cic +++ b/helm/gTopLevel/esempi/sets.cic @@ -1,15 +1,17 @@ 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)) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 0dd76f89a..670978e5c 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -33,18 +33,18 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = 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 | _ -> @@ -57,8 +57,7 @@ let rewrite_tac ~term:equality ~status:(proof,goal) = 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'') @@ -229,9 +228,9 @@ let flin_emult a f = *) 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" ;; @@ -516,88 +515,143 @@ i.e. on obtient une contradiction. *) -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") [];; (******************************************************************************) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 83d959ca3..e5ad5973e 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -63,11 +63,13 @@ let htmlfooter = 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) *) @@ -91,6 +93,38 @@ Arg.parse argspec ignore "" (* 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 = @@ -173,14 +207,21 @@ let applyStylesheets input styles args = ;; 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. *) @@ -201,7 +242,8 @@ let refresh_proof (output : GMathView.math_view) = 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, @@ -220,7 +262,7 @@ let refresh_proof (output : GMathView.math_view) = 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) ;; @@ -740,7 +782,7 @@ let qed rendering_window () = 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) @@ -763,8 +805,9 @@ let qed rendering_window () = (*???? 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 @@ -772,41 +815,49 @@ let save rendering_window () = 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 "\n" ; - Xml.xml_cdata - ("\n\n") ; - xml - >] - in - Xml.pp ~quiet:true xml' (Some prooffile) ; - output_html outputhtml - ("

Current proof saved to " ^ - prooffile ^ "

") + 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 + ("

Current proof type saved to " ^ + prooffiletype ^ "

") ; + Xml.pp ~quiet:true bodyxml (Some prooffile) ; + output_html outputhtml + ("

Current proof body saved to " ^ + prooffile ^ "

") ;; (* 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) ; @@ -818,7 +869,10 @@ let load rendering_window () = refresh_proof output ; refresh_sequent proofw ; output_html outputhtml - ("

Current proof loaded from " ^ + ("

Current proof type loaded from " ^ + prooffiletype ^ "

") ; + output_html outputhtml + ("

Current proof body loaded from " ^ prooffile ^ "

") | _ -> assert false with @@ -977,15 +1031,15 @@ let open_ rendering_window () = 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 @@ -1080,7 +1134,6 @@ let check rendering_window scratch_window () = | None -> None ) context in - (* Do something interesting *) let lexbuf = Lexing.from_string input in try while true do @@ -1094,6 +1147,7 @@ let check rendering_window scratch_window () = 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 @@ -1159,7 +1213,7 @@ let locate rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ;; -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 @@ -1175,7 +1229,7 @@ let backward rendering_window () = 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) @@ -1183,12 +1237,42 @@ let backward rendering_window () = let html = "

Backward Query:

" ^ "

Levels:

" ^ - MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ - " 
" ^ get_last_query result ^ "
" in + MQueryGenerator.string_of_levels + (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" + 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' = + "

^ Exception raised trying to apply " ^ + uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc + in + tl',exc' + in + filter_out uris + in + let html' = + "

Objects that can actually be applied:

" ^ + String.concat "
" uris' ^ exc ^ + "

Number of false matches: " ^ + string_of_int (List.length uris - List.length uris') ^ "

" + 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 @@ -1440,8 +1524,8 @@ class rendering_window output proofw (label : GMisc.label) = 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 @@ -1544,7 +1628,7 @@ object(self) 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)) ; @@ -1584,18 +1668,23 @@ let initialize_everything () = ;; 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 = ("

Locate Query: 

" ^ get_last_query result ^ "
") in + (function uri,_ -> + wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + let html = + ("

Locate Query: 

" ^ get_last_query result ^ "
") + in begin match !rendering_window with None -> assert false @@ -1624,26 +1713,7 @@ let _ = 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 ; diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 4deaf8c7a..1776db1d3 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -64,14 +64,22 @@ let levels_of_term metasenv context term = 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) -> @@ -84,7 +92,7 @@ let levels_of_term metasenv context term = 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 @@ -96,6 +104,11 @@ let levels_of_term metasenv context term = | 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 -> @@ -167,8 +180,9 @@ let execute_query query = 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 @@ -185,10 +199,10 @@ let execute_query query = 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 ( @@ -207,10 +221,11 @@ let backward e c t level = 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 [".*"]) diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli index 57137974f..2e4e59d5c 100644 --- a/helm/gTopLevel/mQueryGenerator.mli +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -50,6 +50,6 @@ val execute_query : MathQL.query -> MathQL.result 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 diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index bf65d1a7b..25d8899d7 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -29,6 +29,7 @@ open ProofEngineTypes exception NotAnInductiveTypeToEliminate exception NotTheRightEliminatorShape exception NoHypothesesFound +exception WrongUriToVariable of string (* TODO problemone del fresh_name, aggiungerlo allo status? *) let fresh_name () = "FOO" @@ -49,7 +50,7 @@ let lambda_abstract context newmeta ty name = 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 @@ -74,7 +75,9 @@ let eta_expand metasenv context t arg = 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 @@ -83,11 +86,17 @@ let eta_expand metasenv context t arg = | 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 @@ -105,6 +114,8 @@ let eta_expand metasenv context t arg = 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 @@ -174,7 +185,7 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = (* 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 = @@ -189,11 +200,56 @@ let new_metasenv_for_apply proof context ty = 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 *) @@ -202,12 +258,51 @@ let apply_tac ~term ~status:(proof, goal) = 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 @@ -216,15 +311,17 @@ let apply_tac ~term ~status:(proof, goal) = 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 @@ -322,11 +419,11 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = 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; @@ -335,7 +432,7 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = 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 @@ -350,10 +447,8 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = 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 diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 5f0ba8aaa..94cc5bd5e 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -31,21 +31,35 @@ open ProofEngineTypes 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]. *) @@ -54,8 +68,7 @@ let metas_in_term term = let module C = Cic in let rec aux = function - C.Rel _ - | C.Var _ -> [] + C.Rel _ -> [] | C.Meta (n,_) -> [n] | C.Sort _ | C.Implicit -> [] @@ -64,15 +77,17 @@ let metas_in_term term = | 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 @@ -223,10 +238,7 @@ let fold term = (*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' = @@ -253,6 +265,7 @@ let fold term = (* 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 ())) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index f5c31067f..b17ba48ba 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -42,6 +42,7 @@ val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term 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 diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index bb724fc75..0446132c5 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -37,47 +37,47 @@ (* 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 @@ -89,23 +89,31 @@ let syntactic_equality ~alpha_equivalence = 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 *) @@ -115,7 +123,8 @@ let replace ~equality ~what ~with_what ~where = 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 @@ -128,12 +137,16 @@ let replace ~equality ~what ~with_what ~where = (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 @@ -161,7 +174,11 @@ let replace_lifting ~equality ~what ~with_what ~where = 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 @@ -189,11 +206,23 @@ let replace_lifting ~equality ~what ~with_what ~where = | _ 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 @@ -230,14 +259,20 @@ let reduce 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.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 *) @@ -264,17 +299,36 @@ let reduce context = 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 -> @@ -307,30 +361,23 @@ let reduce context = | 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 -> @@ -340,7 +387,7 @@ let reduce context = 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) ) @@ -396,6 +443,8 @@ let reduce context = 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 [] ;; @@ -438,15 +487,21 @@ let simpl 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 @@ -472,88 +527,105 @@ let simpl context = 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 -> @@ -584,30 +656,23 @@ let simpl context = | 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 -> @@ -617,7 +682,7 @@ let simpl context = 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) ) @@ -673,6 +738,8 @@ let simpl context = 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 [] ;; diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli index aa0a3a648..f185dd663 100644 --- a/helm/gTopLevel/proofEngineReduction.mli +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -24,8 +24,7 @@ *) exception Impossible of int -exception ReferenceToDefinition -exception ReferenceToAxiom +exception ReferenceToConstant exception ReferenceToVariable exception ReferenceToCurrentProof exception ReferenceToInductiveDefinition @@ -34,7 +33,7 @@ exception RelToHiddenHypothesis 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 diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml index e01f95e9f..d89420f58 100644 --- a/helm/gTopLevel/proofEngineStructuralRules.ml +++ b/helm/gTopLevel/proofEngineStructuralRules.ml @@ -36,7 +36,7 @@ let clearbody ~hyp ~status:(proof, goal) = let string_of_name = function C.Name n -> n - | C.Anonimous -> "_" + | C.Anonymous -> "_" in let metasenv' = List.map @@ -101,7 +101,7 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) = let string_of_name = function C.Name n -> n - | C.Anonimous -> "_" + | C.Anonymous -> "_" in let metasenv' = List.map diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli index f6ee6a529..32ba812ac 100644 --- a/helm/gTopLevel/proofEngineStructuralRules.mli +++ b/helm/gTopLevel/proofEngineStructuralRules.mli @@ -1,2 +1,27 @@ +(* 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 diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 953ed6444..1d614b6f6 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -48,8 +48,13 @@ let warn s = 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) @@ -63,8 +68,7 @@ let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" 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) @@ -72,28 +76,41 @@ let applus_uri = (apolynomial_uri, 0, 4) 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 *) @@ -157,30 +174,29 @@ let context_of_status ~status:(proof, goal as status) = 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 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 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 *) @@ -195,12 +211,12 @@ exception GoalUnringable (** 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 @@ -238,17 +254,17 @@ let split_eq = 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. @@ -259,15 +275,12 @@ let path_of_int n proof = / \ 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 *) @@ -278,9 +291,9 @@ let btree_of_array ~vars ~proof = 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 @@ -288,11 +301,10 @@ let btree_of_array ~vars ~proof = abstraction function: concrete polynoms -----> (abstract polynoms, varmap) @param terms list of conrete polynoms - @param proof current proof @return a pair 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 *) @@ -300,23 +312,23 @@ let abstract_poly ~terms ~proof = (* "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; @@ -326,7 +338,7 @@ let abstract_poly ~terms ~proof = 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) @@ -338,36 +350,52 @@ let abstract_poly ~terms ~proof = 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]) @@ -407,7 +435,7 @@ let elim_type2_tac ~term ~proof ~status = *) 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 -> @@ -448,15 +476,14 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = 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) -> @@ -471,13 +498,19 @@ let ring_tac ~status:(proof, goal) = 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 @@ -506,11 +539,16 @@ let ring_tac ~status:(proof, goal) = ~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 diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index d0430162e..ad8d5bd1d 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -30,7 +30,7 @@ module TextualPp = let print_name = function Cic.Name n -> n - | Cic.Anonimous -> "_" + | Cic.Anonymous -> "_" in List.fold_right (fun i (output,context) -> @@ -62,6 +62,8 @@ module TextualPp = 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 @@ -70,41 +72,43 @@ module XmlPp = 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 "\n" ; + X.xml_cdata ("\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 ;; diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml index f3cd13b44..b8490f059 100644 --- a/helm/gTopLevel/tacticals.ml +++ b/helm/gTopLevel/tacticals.ml @@ -31,7 +31,7 @@ open UriManager (** DEBUGGING *) (** perform debugging output? *) -let debug = false +let debug = true (** debugging print *) let warn s = diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index d53ea70ea..78aceae26 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -39,10 +39,9 @@ let get_terms () = 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 _ -> diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/gTopLevel/xml2Gdome.ml index 8c6298d09..c4e9445eb 100644 --- a/helm/gTopLevel/xml2Gdome.ml +++ b/helm/gTopLevel/xml2Gdome.ml @@ -27,6 +27,8 @@ let document_of_xml (domImplementation : Gdome.domImplementation) strm = let module G = Gdome in let module X = Xml in let root_name,root_attributes,root_content = + ignore (Stream.next strm) ; (* to skip the 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