{ K.conclude_id = gen_id conclude_prefix seed;
K.conclude_aref = id;
K.conclude_method = "Exact";
- K.conclude_args = [K.Term t];
+ K.conclude_args = [K.Term (false, t)];
K.conclude_conclusion =
try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
with Not_found -> None
}
;;
-let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
+let infer_dependent ~headless context metasenv = function
+ | [] -> assert false
+ | [t] -> [false, t]
+ | he::tl as l ->
+ if headless then
+ List.map (function s -> false,s) l
+ else
+ try
+ let hety,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv context (Deannotate.deannotate_term he)
+ CicUniv.oblivion_ugraph
+ in
+ let fstorder t =
+ match CicReduction.whd context t with
+ | Cic.Prod _ -> false
+ | _ -> true
+ in
+ let rec dummify_last_tgt t =
+ match CicReduction.whd context t with
+ | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt)
+ | _ -> Cic.Implicit None
+ in
+ let rec aux ty = function
+ | [] -> []
+ | t::tl ->
+ match
+ FreshNamesGenerator.clean_dummy_dependent_types
+ (dummify_last_tgt ty)
+ with
+ | Cic.Prod (n,src,tgt) ->
+ (n <> Cic.Anonymous && fstorder src, t) ::
+ aux (CicSubstitution.subst
+ (Deannotate.deannotate_term t) tgt) tl
+ | _ -> assert false
+ in
+ (false, he) :: aux hety tl
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+;;
+
+let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
let module C = Cic in
let module K = Content in
let rec aux =
function
[] -> [],[]
- | t::l1 ->
+ | (dep, t)::l1 ->
let subproofs,args = aux l1 in
if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
let new_subproof =
acic2content
- seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+ seed context metasenv
+ ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
let new_arg =
K.Premise
{ K.premise_id = gen_id premise_prefix seed;
K.premise_binder = Some b;
K.premise_n = Some n
}
- else (K.Term t)
+ else (K.Term (dep,t))
| C.AConst(id,uri,[]) ->
let sort =
(try
K.lemma_name = UriManager.name_of_uri uri;
K.lemma_uri = UriManager.string_of_uri uri
}
- else (K.Term t)
+ else (K.Term (dep,t))
| C.AMutConstruct(id,uri,tyno,consno,[]) ->
let sort =
(try
string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
")"
}
- else (K.Term t)
- | _ -> (K.Term t)) in
+ else (K.Term (dep,t))
+ | _ -> (K.Term (dep,t))) in
subproofs,hd::args
in
- match (aux l) with
+ match (aux (infer_dependent ~headless context metasenv l)) with
[p],args ->
[{p with K.proof_name = None}],
List.map
and
-build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ~ids_to_inner_sorts ~ids_to_inner_types =
let module K = Content in
try
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
(let p =
- (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
+ (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
in
`Proof p;)
else
Prop. For debugging purposes this is tested again, possibly raising an
Not_a_proof exception *)
-and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
- let rec aux ?name t =
+and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
+ let rec aux ?name context t =
let module C = Cic in
let module K = Content in
let module C2A = Cic2acic in
| C.ASort (id,s) -> raise Not_a_proof
| C.AImplicit _ -> raise NotImplemented
| C.AProd (_,_,_,_) -> raise Not_a_proof
- | C.ACast (id,v,t) -> aux v
+ | C.ACast (id,v,t) -> aux context v
| C.ALambda (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = aux t in
+ let proof =
+ aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t
+ in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
match proof.K.proof_conclude.K.conclude_args with
| C.ALetIn (id,n,s,t) ->
let sort = Hashtbl.find ids_to_inner_sorts id in
if sort = `Prop then
- let proof = aux t in
+ let proof = (* XXX TIPAMI!!! *)
+ aux ((Some (n,Cic.Def (Deannotate.deannotate_term s,None)))::context) t
+ in
let proof' =
if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
match proof.K.proof_conclude.K.conclude_args with
{ proof' with
K.proof_name = None;
K.proof_context =
- ((build_def_item seed (get_id s) n s ids_to_inner_sorts
+ ((build_def_item seed context metasenv (get_id s) n s ids_to_inner_sorts
ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
::proof'.K.proof_context;
}
raise Not_a_proof
| C.AAppl (id,li) ->
(try coercion
- seed li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try rewrite
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try inductive
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try transitivity
- seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
let subproofs, args =
build_subproofs_and_args
- seed li ~ids_to_inner_types ~ids_to_inner_sorts in
+ seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in
(*
let args_to_lift =
List.filter (test_for_lifting ~ids_to_inner_types) li in
let pp =
let build_proof p (name,arity) =
let rec make_context_and_body c p n =
- if n = 0 then c,(aux p)
+ if n = 0 then c,(aux context p)
else
(match p with
Cic.ALambda(idl,vname,s1,t1) ->
let ce =
- build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
+ build_decl_item
+ seed idl vname s1 ~ids_to_inner_sorts in
make_context_and_body (ce::c) t1 (n-1)
| _ -> assert false) in
let context,body = make_context_and_body [] p arity in
List.map2 build_proof patterns name_and_arities in
let context,term =
(match
- build_subproofs_and_args
- seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
+ build_subproofs_and_args ~headless:true
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te]
with
l,[t] -> l,t
| _ -> assert false) in
K.conclude_method = "Case";
K.conclude_args =
(K.Aux (UriManager.string_of_uri uri))::
- (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+ (K.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp;
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
}
}
| C.AFix (id, no, funs) ->
+ let context' =
+ List.fold_left
+ (fun ctx (_,n,_,ty,_) ->
+ let ty = Deannotate.deannotate_term ty in
+ Some (Cic.Name n,Cic.Decl ty) :: ctx)
+ [] funs @ context
+ in
let proofs =
List.map
- (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+ (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in
let fun_name =
List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no
in
}
}
| C.ACoFix (id,no,funs) ->
+ let context' =
+ List.fold_left
+ (fun ctx (_,n,ty,_) ->
+ let ty = Deannotate.deannotate_term ty in
+ Some (Cic.Name n,Cic.Decl ty) :: ctx)
+ [] funs @ context
+ in
let proofs =
List.map
- (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
+ (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in
let jo =
{ K.joint_id = gen_id joint_prefix seed;
K.joint_kind = `CoRecursive;
in
let id = get_id t in
generate_conversion seed false id t1 ~ids_to_inner_types
-in aux ?name t
+in aux ?name context t
-and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
- let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
+and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+ let aux context ?name =
+ acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
let args_for_cases, other_args =
split no_constructors tail_args in
let subproofs,other_method_args =
- build_subproofs_and_args seed other_args
- ~ids_to_inner_types ~ids_to_inner_sorts in
+ build_subproofs_and_args ~headless:true seed context metasenv
+ other_args ~ids_to_inner_types ~ids_to_inner_sorts in
let method_args=
let rec build_method_args =
function
let hdarg =
if sortarg = `Prop then
let (co,bo) =
- let rec bc =
+ let rec bc context =
function
Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
+ let context' =
+ Some (n,Cic.Decl(Deannotate.deannotate_term s1))
+ ::context
+ in
let ce =
build_decl_item
seed idl n s1 ~ids_to_inner_sorts in
if (occur ind_uri s) then
( match t1 with
Cic.ALambda(id2,n2,s2,t2) ->
+ let context'' =
+ Some
+ (n2,Cic.Decl
+ (Deannotate.deannotate_term s2))
+ ::context'
+ in
let inductive_hyp =
`Hypothesis
{ K.dec_name = name_of n2;
K.dec_aref = id2;
K.dec_type = s2
} in
- let (context,body) = bc (t,t2) in
+ let (context,body) = bc context'' (t,t2) in
(ce::inductive_hyp::context,body)
| _ -> assert false)
else
(
- let (context,body) = bc (t,t1) in
+ let (context,body) = bc context' (t,t1) in
(ce::context,body))
- | _ , t -> ([],aux t) in
- bc (ty,arg) in
+ | _ , t -> ([],aux context t) in
+ bc context (ty,arg) in
K.ArgProof
{ bo with
K.proof_name = Some name;
K.proof_context = co;
};
- else (K.Term arg) in
+ else (K.Term (false,arg)) in
hdarg::(build_method_args (tlc,tla))
| _ -> assert false in
build_method_args (constructors1,args_for_cases) in
K.conclude_method = method_name;
K.conclude_args =
K.Aux (string_of_int no_constructors)
- ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
+ ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))))
::method_args@other_method_args;
K.conclude_conclusion =
try Some
}
| _ -> raise NotApplicable
-and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
match li with
| ((Cic.AConst _) as he)::tl
| ((Cic.AMutInd _) as he)::tl
| [t] -> t
| _::tl -> last tl
in
- acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
| _ -> raise NotApplicable
-and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
- let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
+and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+ let aux context ?name =
+ acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ in
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
let subproofs,arg =
(match
build_subproofs_and_args
- seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
+ seed context metasenv
+ ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
with
l,[p] -> l,p
| _,_ -> assert false) in
let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
with Not_found -> `Type (CicUniv.fresh())) in
if asort = `Prop then
- K.ArgProof (aux a)
- else K.Term a in
+ K.ArgProof (aux context a)
+ else K.Term (false,a) in
hd::(ma_aux (n-1) tl) in
(ma_aux 3 args) in
{ K.proof_name = name;
K.conclude_aref = id;
K.conclude_method = "Rewrite";
K.conclude_args =
- K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
+ K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
else raise NotApplicable
| _ -> raise NotApplicable
-and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+and transitivity
+ seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
+=
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
K.conclude_aref = id;
K.conclude_method = "Eq_chain";
K.conclude_args =
- K.Term t1::
+ K.Term (false,t1)::
(transitivity_aux
- seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
- [K.Term t2]@
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @ [K.Term (false,t2)]@
(transitivity_aux
- seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
- [K.Term t3];
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ @ [K.Term (false,t3)];
K.conclude_conclusion =
try Some
(Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
}
| _ -> raise NotApplicable
-and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
+and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t =
let module C2A = Cic2acic in
let module K = Content in
let module C = Cic in
| [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
| _ -> raise NotApplicable
in
- (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
- @[K.Term t2]
- @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
+ (transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+ @[K.Term (false,t2)]
+ @(transitivity_aux
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
| _ -> [K.ArgProof
- (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
+ (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)]
;;
(map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
conjectures),
`Def (K.Const,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item
+ seed [] (Deannotate.deannotate_conjectures conjectures)
+ (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (_,_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Const,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AConstant (id,_,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
| C.AVariable (_,n,Some bo,ty,params,_) ->
(gen_id object_prefix seed, params, None,
`Def (K.Var,ty,
- build_def_item seed (get_id bo) (C.Name n) bo
+ build_def_item seed [] [] (get_id bo) (C.Name n) bo
~ids_to_inner_sorts ~ids_to_inner_types))
| C.AVariable (id,n,None,ty,params,_) ->
(gen_id object_prefix seed, params, None,
Aux of string
| Premise of premise
| Lemma of lemma
- | Term of 'term
+ | Term of bool * 'term
| ArgProof of 'term proof
| ArgMethod of string (* ???? *)
Aux of string
| Premise of premise
| Lemma of lemma
- | Term of 'term
+ | Term of bool * 'term (* inferrable, term *)
| ArgProof of 'term proof
| ArgMethod of string (* ???? *)
| _ -> prerr_endline "2"; assert false)
else if conclude.Con.conclude_method = "Exact" then
(match conclude.Con.conclude_args with
- [Con.Term t] -> deannotate t
+ [Con.Term (_,t)] -> deannotate t
| [Con.Premise prem] ->
(match prem.Con.premise_n with
None -> assert false
conclude.Con.conclude_method = "Exists" ||
conclude.Con.conclude_method = "FalseInd") then
(match (List.tl conclude.Con.conclude_args) with
- Con.Term (C.AAppl (
+ Con.Term (_,C.AAppl (
id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
| _ -> prerr_endline "5"; assert false)
else if (conclude.Con.conclude_method = "Rewrite") then
(match conclude.Con.conclude_args with
- Con.Term (C.AConst (sid,uri,exp_named_subst))::args ->
+ Con.Term (_,C.AConst (sid,uri,exp_named_subst))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in
| _ -> prerr_endline "6"; assert false)
else if (conclude.Con.conclude_method = "Case") then
(match conclude.Con.conclude_args with
- Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+ Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Premise(prem)::patterns ->
C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty,
(function
Con.ArgProof p -> proof2cic [] p
| _ -> prerr_endline "7a"; assert false) patterns)
- | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
+ | Con.Aux(uri)::Con.Aux(notype)::Con.Term(_,ty)::Con.Term(_,te)::patterns -> C.MutCase
(UriManager.uri_of_string uri,
int_of_string notype, deannotate ty, deannotate te,
List.map
raise Not_found))
| Con.Lemma lemma ->
CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
- | Con.Term t -> deannotate t
+ | Con.Term (_,t) -> deannotate t
| Con.ArgProof p -> proof2cic [] p (* empty! *)
| Con.ArgMethod s -> raise TO_DO
List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
;;
+let deannotate_conjectures =
+ let module C = Cic in
+ List.map
+ (function
+ (_,id,acontext,con) ->
+ let context =
+ List.map
+ (function
+ | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None)))
+ | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
+ | _,None -> None)
+ acontext
+ in
+ (id,context,deannotate_term con))
+;;
+
let deannotate_obj =
let module C = Cic in
function
| C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
C.CurrentProof (
name,
- List.map
- (function
- (_,id,acontext,con) ->
- let context =
- List.map
- (function
- _,Some (n,(C.ADef at)) ->
- Some (n,(C.Def ((deannotate_term at),None)))
- | _,Some (n,(C.ADecl at)) ->
- Some (n,(C.Decl (deannotate_term at)))
- | _,None -> None
- ) acontext
- in
- (id,context,deannotate_term con)
- ) conjs,
+ deannotate_conjectures conjs,
deannotate_term bo,deannotate_term ty, params, attrs
)
| C.AInductiveDefinition (_, tys, params, parno, attrs) ->
(******************************************************************************)
val deannotate_term : Cic.annterm -> Cic.term
+val deannotate_conjectures : Cic.annmetasenv -> Cic.metasenv
val deannotate_obj : Cic.annobj -> Cic.obj
exception Error of int * int * string
let regexp number = xml_digit+
+let regexp utf8_blank = " " | "\n" | "\t" | [160] (* this is a nbsp *)
(* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
(* let regexp ident_letter = xml_letter *)
let regexp meta_anonymous = "$_"
let regexp qstring = '"' [^ '"']* '"'
-let regexp begincomment = "(**" xml_blank
+let regexp begincomment = "(**" utf8_blank
let regexp beginnote = "(*"
let regexp endcomment = "*)"
(* let regexp comment_char = [^'*'] | '*'[^')']
let rec level2_meta_token =
lexer
- | xml_blank+ -> level2_meta_token lexbuf
+ | utf8_blank+ -> level2_meta_token lexbuf
| ident ->
let s = Ulexing.utf8_lexeme lexbuf in
begin
and level2_ast_token =
lexer
- | xml_blank+ -> ligatures_token level2_ast_token lexbuf
+ | utf8_blank+ -> ligatures_token level2_ast_token lexbuf
| meta ->
let s = Ulexing.utf8_lexeme lexbuf in
return lexbuf ("META", String.sub s 1 (String.length s - 1))
and level1_pattern_token =
lexer
- | xml_blank+ -> ligatures_token level1_pattern_token lexbuf
+ | utf8_blank+ -> ligatures_token level1_pattern_token lexbuf
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
| ident ->
let s = Ulexing.utf8_lexeme lexbuf in
Some "xlink", "href", lemma.Con.lemma_uri ]
in
(B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row
- | Con.Term t ->
- if is_first then
+ | Con.Term (b,t) ->
+ if is_first || (not b) then
(term2pres t)::row
else (B.b_object (P.Mi([],"?")))::row
| Con.ArgProof _
Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])
and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
- let rec proof2pres ?(skip_initial_lambdas_internal=false) is_top_down p omit_dot =
- prerr_endline p.Con.proof_conclude.Con.conclude_method;
+ let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot =
let indent =
let is_decl e =
(match e with
| Some t -> Some (term2pres t)) in
let body =
let presconclude =
- conclude2pres ~skip_initial_lambdas_internal is_top_down p.Con.proof_conclude indent omit_conclusion
+ conclude2pres
+ ?skip_initial_lambdas_internal:
+ (match skip_initial_lambdas_internal with
+ Some (`Later s) -> Some (`Now s)
+ | _ -> None)
+ is_top_down
+ p.Con.proof_name p.Con.proof_conclude indent omit_conclusion
omit_dot in
let presacontext =
acontext2pres
(p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
in
context2pres
- (if skip_initial_lambdas_internal then [] else p.Con.proof_context)
+ (match skip_initial_lambdas_internal with
+ Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
+ | _ -> p.Con.proof_context)
presacontext
in
match p.Con.proof_name with
let concl =
make_concl ~attrs:[ Some "helm", "xref", p.Con.proof_id ]
"proof of" ac in
- B.b_toggle [ concl; body ]
+ B.b_toggle [ B.H ([], [concl; B.skip ; B.Text([],"(");
+ B.Object ([], P.Mi ([],name));
+ B.Text([],")") ]) ; body ]
in
B.indent action
[B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
continuation])) ac continuation
- and conclude2pres ?skip_initial_lambdas_internal is_top_down conclude indent omit_conclusion omit_dot =
+ and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot =
let tconclude_body =
match conclude.Con.conclude_conclusion with
Some t (*when not omit_conclusion or
if conclude.Con.conclude_method = "BU_Conversion" then
B.b_hv []
(make_concl "that is equivalent to" concl ::
- if is_top_down then [B.b_space ; B.Text([],"done.")] else [])
+ if is_top_down then [B.b_space ; B.b_kw "done";
+ B.Text([],".")] else [])
else if conclude.Con.conclude_method = "FalseInd" then
(* false ind is in charge to add the conclusion *)
falseind conclude
else
+ let prequel =
+ if
+ (match skip_initial_lambdas_internal with
+ None
+ | Some (`Later _) -> true
+ | Some (`Now _) -> false)
+ && conclude.Con.conclude_method = "Intros+LetTac"
+ then
+ let name = get_name name in
+ [B.V ([],
+ [ B.H([],
+ let expected =
+ (match conclude.Con.conclude_conclusion with
+ None -> B.Text([],"NO EXPECTED!!!")
+ | Some c -> term2pres c)
+ in
+ [make_concl "we need to prove" expected;
+ B.skip;
+ B.Text([],"(");
+ B.Object ([], P.Mi ([],name));
+ B.Text([],")");
+ B.Text ([],".")
+ ])])]
+ else
+ [] in
let conclude_body =
conclude_aux ?skip_initial_lambdas_internal conclude in
let ann_concl =
|| conclude.Con.conclude_method = "TD_Conversion"
then
B.Text([],"")
- else if omit_conclusion then B.Text([],"done.")
+ else if omit_conclusion then
+ B.H([], [B.b_kw "done" ; B.Text([],".") ])
else B.b_hv []
- ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else [])
+ ((if not is_top_down || omit_dot then [make_concl "we proved"
+ concl; B.Text([],if not is_top_down then "(previous)" else "")]
+ else [B.b_kw "done"]) @ if not omit_dot then [B.Text([],".")] else [])
in
- B.V ([], [conclude_body; ann_concl])
+ B.V ([], prequel @ [conclude_body; ann_concl])
| _ -> conclude_aux ?skip_initial_lambdas_internal conclude
in
if indent then
else if conclude.Con.conclude_method = "Exact" then
let arg =
(match conclude.Con.conclude_args with
- [Con.Term t] -> term2pres t
+ [Con.Term (b,t)] -> assert (not b);term2pres t
| [Con.Premise p] ->
(match p.Con.premise_binder with
| None -> assert false; (* unnamed hypothesis ??? *)
(match conclude.Con.conclude_conclusion with
None ->
B.b_h [] [B.b_kw "by"; B.b_space; arg]
- | Some c -> let conclusion = term2pres c in
+ | Some c ->
B.b_h [] [B.b_kw "by"; B.b_space; arg]
)
else if conclude.Con.conclude_method = "Intros+LetTac" then
(match conclude.Con.conclude_args with
- [Con.ArgProof p] -> proof2pres ?skip_initial_lambdas_internal true p false
+ [Con.ArgProof p] ->
+ (match conclude.Con.conclude_args with
+ [Con.ArgProof p] ->
+ proof2pres ?skip_initial_lambdas_internal true p false
+ | _ -> assert false)
| _ -> assert false)
(* OLD CODE
let conclusion =
| _ -> assert false) in
let term1 =
(match List.nth conclude.Con.conclude_args 2 with
- Con.Term t -> term2pres t
+ Con.Term (_,t) -> term2pres t
| _ -> assert false) in
let term2 =
(match List.nth conclude.Con.conclude_args 5 with
- Con.Term t -> term2pres t
+ Con.Term (_,t) -> term2pres t
| _ -> assert false) in
(*
B.V ([],
*) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"])
else if conclude.Con.conclude_method = "Eq_chain" then
let justification p =
+(*
if skip_initial_lambdas <> None (* cheating *) then
[B.b_kw "by _"]
else
+*)
let j1,j2 = justification term2pres p in
j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
in
let rec aux args =
match args with
| [] -> []
- | (Con.ArgProof p)::(Con.Term t)::tl ->
+ | (Con.ArgProof p)::(Con.Term (_,t))::tl ->
B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
"=";B.b_space;term2pres t;B.b_space]@justification p@
(if tl <> [] then [B.Text ([],".")] else [])))::(aux tl)
in
let hd =
match List.hd conclude.Con.conclude_args with
- | Con.Term t -> t
+ | Con.Term (_,t) -> t
| _ -> assert false
in
- B.HOV([],[B.Text ([],"conclude");B.b_space;term2pres hd; (* B.b_space; *)
+ B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *)
B.V ([],aux (List.tl conclude.Con.conclude_args))])
else if conclude.Con.conclude_method = "Apply" then
let pres_args =
Con.Aux n -> B.b_kw ("aux " ^ n)
| Con.Premise prem -> B.b_kw "premise"
| Con.Lemma lemma -> B.b_kw "lemma"
- | Con.Term t -> term2pres t
+ | Con.Term (_,t) -> term2pres t
| Con.ArgProof p -> proof2pres true p false
| Con.ArgMethod s -> B.b_kw "method"
None -> B.b_kw "the previous result"
| Some n -> B.Object ([], P.Mi([],n)))
| Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
- | Con.Term t ->
+ | Con.Term (_,t) ->
term2pres t
| Con.ArgProof p -> B.b_kw "a proof???"
| Con.ArgMethod s -> B.b_kw "a method???")
None -> B.b_kw "the previous result"
| Some n -> B.Object ([], P.Mi([],n)))
| Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
- | Con.Term t ->
+ | Con.Term (_,t) ->
term2pres t
| Con.ArgProof p -> B.b_kw "a proof???"
| Con.ArgMethod s -> B.b_kw "a method???") in
(* let acontext =
acontext2pres_old p.Con.proof_apply_context true in *)
let body =
- conclude2pres true p.Con.proof_conclude true true false in
+ conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in
let presacontext =
let acontext_id =
match p.Con.proof_apply_context with
B.skip;
term2pres hyp2.Con.dec_type]) in
(* let body = proof2pres {proof with Con.proof_context = tl} false in *)
- let body= conclude2pres false proof.Con.proof_conclude false true false in
+ let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in
let presacontext =
acontext2pres false proof.Con.proof_apply_context body false false
in
B.skip;
term2pres hyp.Con.dec_type]) in
(* let body = proof2pres {proof with Con.proof_context = tl} false in *)
- let body= conclude2pres false proof.Con.proof_conclude false true false in
+ let body= conclude2pres false proof.Con.proof_name proof.Con.proof_conclude false true false in
let presacontext =
acontext2pres false proof.Con.proof_apply_context body false false
in
| _ -> assert false
in
- proof2pres ?skip_initial_lambdas_internal:skip_initial_lambdas is_top_down p false
+ proof2pres
+ ?skip_initial_lambdas_internal:
+ (match skip_initial_lambdas with
+ None -> Some (`Later 0) (* we already printed theorem: *)
+ | Some n -> Some (`Later n))
+ is_top_down p false
exception ToDo
(**************************************************************************)
val content2pres:
- ?skip_initial_lambdas:bool -> ?skip_thm_and_qed:bool ->
+ ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool ->
ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
Cic.annterm Content.cobj ->
CicNotationPres.boxml_markup
HLog.debug "Warning SELECT without REGEXP";
sprintf
("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence LIKE '%s%%'")
+ "h_occurrence LIKE '%s%%' ESCAPE \"\\\"")
obj_tbl buri*)
end
in
HLog.debug "Warning SELECT without REGEXP";
sprintf
("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence LIKE '%s%%'")
+ "h_occurrence LIKE '%s%%' ESCAPE \"\\\" ")
obj_tbl buri
*)
end
let xpointers_of_ind uri =
let dbd = instance () in
let name_tbl = MetadataTypes.name_tbl () in
+ let escape s =
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ in
let query = sprintf
- "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl
- (HSql.escape (UriManager.string_of_uri uri))
+ "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' ESCAPE \"\\\" "
+ name_tbl (escape (UriManager.string_of_uri uri))
in
let rc = HSql.exec dbd query in
let l = ref [] in
uris
in
let del_from tbl =
+ let escape s =
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ in
let query s =
- sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s
+ sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\" ESCAPE \"\\\" "
+ (tbl ()) (escape s)
in
List.iter
(fun source_col -> ignore (HSql.exec dbd (query source_col)))
let unindex ~dbd ~uri =
let uri = UriManager.string_of_uri uri in
let del_from tbl =
+ let escape s =
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ in
let query tbl =
- sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri
+ sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\" ESCAPE \"\\\" "
+ (tbl ()) (escape uri)
in
ignore (HSql.exec dbd (query tbl))
in
let sorted_uris_of_baseuri ~dbd baseuri =
let sql_pat =
- Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" baseuri ^ "%"
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%"
in
let query =
Printf.sprintf
- ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^
- "SELECT source FROM %s WHERE source LIKE \"%s\"")
+ ("SELECT source FROM %s WHERE source LIKE \"%s\" ESCAPE \"\\\" UNION "
+ ^^
+ "SELECT source FROM %s WHERE source LIKE \"%s\" ESCAPE \"\\\"")
(MetadataTypes.name_tbl ()) sql_pat
MetadataTypes.library_name_tbl sql_pat
in
let move_content (name1, tbl1) (name2, tbl2) buri =
+ let escape s =
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ in
assert (tbl1 = tbl2);
sprintf
"INSERT INTRO %s SELECT * FROM %s WHERE source LIKE \"%s%%\";"
- name2 name1 (HSql.escape buri)
+ name2 name1 (escape buri)
let direct_deps refObj uri =
sprintf "SELECT * FROM %s WHERE source = \"%s\";"
let lambda_close ?prefix_name t menv ctx =
let t = naif_closure ?prefix_name t menv ctx in
List.fold_left
- (fun t -> function
- | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *)
- | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
- | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t))
- t ctx
+ (fun (t,i) -> function
+ | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+ | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+ | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1)
+ (t,List.length menv) ctx
;;
(* functions for retrieving theorems *)
args
in
if propositional_args = [] then
- let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+ let newmetas =
+ List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
+ in
Some (args,metasenv,newmetas,head,newmeta)
else None
;;
candidates
;;
-let only signature context t =
+let only signature context metasenv t =
try
- let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
+ in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
if b then b
else
- try
- let ty' = unfold context ty in
- let consts' = MetadataConstraints.constants_of ty' in
- MetadataConstraints.UriManagerSet.subset consts' signature
- with _-> false
- with _ -> false
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> assert false
+ | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
;;
let not_default_eq_term t =
not (LibraryObjects.in_eq_URIs uri)
with Invalid_argument _ -> true
-let retrieve_equations signature universe cache context=
+let retrieve_equations dont_filter signature universe cache context metasenv =
match LibraryObjects.eq_URI() with
| None -> []
| Some eq_uri ->
let fake= Cic.Meta(-1,[]) in
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let candidates = get_candidates universe cache fake_eq in
- (* defaults eq uris are built-in in auto *)
- let candidates = List.filter not_default_eq_term candidates in
- let candidates = List.filter (only signature context) candidates in
- List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
- candidates
+ if dont_filter then candidates
+ else
+ let candidates = List.filter not_default_eq_term candidates in
+ List.filter (only signature context metasenv) candidates
let build_equality bag head args proof newmetas maxmeta =
match head with
let partition_unit_equalities context metasenv newmeta bag equations =
List.fold_left
(fun (units,other,maxmeta)(t,ty) ->
+ if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
+ let _ =
+ HLog.warn
+ ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
+ ^ " since it is not meta closed")
+ in
+ units,(t,ty)::other,maxmeta
+ else
match is_unit_equation context metasenv maxmeta ty with
| Some (args,metasenv,newmetas,head,newmeta') ->
let maxmeta,equality =
Saturation.make_passive [],
Equality.mk_equality_bag)
-let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+let init_cache_and_tables
+ ?dbd use_library paramod use_context dont_filter universe (proof, goal)
+=
(* the local cache in initially empty *)
let cache = AutoCache.cache_empty in
let _, metasenv, _subst,_, _, _ = proof in
let signature = MetadataQuery.signature_of metasenv goal in
let newmeta = CicMkImplicit.new_meta metasenv [] in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let ct = find_context_theorems context metasenv in
+ let ct = if use_context then find_context_theorems context metasenv else [] in
debug_print
(lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
let lt =
- if use_library then
- find_library_theorems dbd metasenv goal
- else [] in
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
debug_print
(lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
let cache = cache_add_list cache context (ct@lt) in
let equations =
- retrieve_equations signature universe cache context in
+ retrieve_equations dont_filter signature universe cache context metasenv
+ in
debug_print
(lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
let eqs_and_types =
HExtlib.filter_map
(fun t ->
let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
- (* retrieve_equations could also return flexible terms *)
- if is_an_equality ty then Some(t,ty)
- else
- try
- let ty' = unfold context ty in
- if is_an_equality ty' then Some(t,ty') else None
- with _ -> None) (* catturare l'eccezione giusta di unfold *)
- equations in
+ CicTypeChecker.type_of_aux'
+ metasenv context t CicUniv.empty_ugraph
+ in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ equations
+ in
let bag = Equality.mk_equality_bag () in
let units, other_equalities, newmeta =
- partition_unit_equalities context metasenv newmeta bag eqs_and_types in
- (* let env = (metasenv, context, CicUniv.empty_ugraph) in
- let equalities =
- let eq_uri =
- match LibraryObjects.eq_URI() with
- | None ->assert false
- | Some eq_uri -> eq_uri in
- Saturation.simplify_equalities bag eq_uri env units in *)
+ partition_unit_equalities context metasenv newmeta bag eqs_and_types
+ in
+ (* SIMPLIFICATION STEP
+ let equalities =
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
+ Saturation.simplify_equalities bag eq_uri env units
+ in
+ *)
let passive = Saturation.make_passive units in
let no = List.length units in
let active = Saturation.make_active [] in
let proof, goalno = status in
let _, metasenv,_subst,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
- let equations = retrieve_equations signature universe cache context in
+ let equations =
+ retrieve_equations false signature universe cache context metasenv
+ in
let eqs_and_types =
HExtlib.filter_map
(fun t ->
in
match
let (active, passive,bag), cache, maxmeta =
- init_cache_and_tables dbd flags.use_library true universe
+ init_cache_and_tables ~dbd flags.use_library true true false universe
(proof'''',newmeta)
in
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
(* just for testing *)
let use_library = flags.use_library in
let tables,cache,newmeta =
- init_cache_and_tables dbd use_library flags.use_only_paramod
- universe (proof, goal) in
+ init_cache_and_tables ~dbd use_library flags.use_only_paramod true
+ false universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
close_more
| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
+(* performs steps of rewrite with the universe, obtaining if possible
+ * a trivial goal *)
+let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)=
+ let _,metasenv,_subst,_,_,_ = proof in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let eq_uri = eq_of_goal ty in
+ let (active,passive,bag), cache, maxm =
+ (* we take the whole universe (no signature filtering) *)
+ init_cache_and_tables false true false true universe (proof,goal)
+ in
+ let initgoal = [], [], ty in
+ let table =
+ let equalities = (Saturation.list_of_passive passive) in
+ (* we demodulate using both actives passives *)
+ List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
+ in
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ match Indexing.solve_demodulating bag env table initgoal steps with
+ | Some (proof, metasenv, newty) ->
+ let refl =
+ match newty with
+ | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
+ Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
+ | _ -> assert false
+ in
+ let proofterm,_ =
+ Equality.build_goal_proof
+ bag eq_uri proof refl newty [] context metasenv
+ in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) status
+ | None ->
+ raise
+ (ProofEngineTypes.Fail (lazy
+ ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+let solve_rewrite_tac ~universe ?steps () =
+ ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps)
+;;
+
(* DEMODULATE *)
let demodulate_tac ~dbd ~universe (proof,goal)=
let curi,metasenv,_subst,pbo,pty, attrs = proof in
let initgoal = [], [], ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd false true universe (proof,goal) in
+ init_cache_and_tables
+ ~dbd false true true false universe (proof,goal)
+ in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
universe:Universe.universe ->
ProofEngineTypes.tactic
+val solve_rewrite_tac:
+ universe:Universe.universe ->
+ ?steps:int ->
+ unit ->
+ ProofEngineTypes.tactic
+
type auto_status =
Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
(int * Cic.term * int) list *
val give_prune_hint : int -> unit
val lambda_close :
- ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term
+ ?prefix_name:string -> Cic.term -> Cic.metasenv -> Cic.context -> Cic.term *
+ int
val pp_proofterm: Cic.term -> string
val revision : string (* svn revision *)
Tacticals.first
[Tactics.auto ~dbd ~params ~universe ;
Tactics.auto ~dbd ~params:params' ~universe]
- | `Term just -> Tactics.apply just
+ | `Term just ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context just
+ CicUniv.empty_ugraph
+ in
+ Tactics.solve_rewrite
+ ~universe:(Universe.index Universe.empty
+ (Universe.key ty) just) ~steps:1 ()
+ (* Tactics.apply just *)
in
let plhs,prhs,prepare =
match lhs with
as above, but finds all the matching equalities, and the matching condition
can be either Founif.matching or Inference.unification
*)
+(* XXX termty unused *)
let rec find_all_matches ?(unif_fun=Founif.unification)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
(*
returns true if target is subsumed by some equality in table
*)
+(*
let print_res l =
prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
((pos,equation),_)) -> Equality.string_of_equality equation)l))
;;
+*)
let subsumption_aux use_unification env table target =
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
| None -> do_right ()
;;
+type next = L | R
+type solved = Yes of Equality.goal | No of Equality.goal list
+
+(* returns all the 1 step demodulations *)
+module C = Cic;;
+module S = CicSubstitution;;
+let rec demodulation_all_aux
+ metasenv context ugraph table lift_amount term
+=
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term
+ in
+ match term with
+ | C.Meta _ -> []
+ | _ ->
+ let termty, ugraph = C.Implicit None, ugraph in
+ let res =
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
+ in
+ match term with
+ | C.Appl l ->
+ let res, _, _ =
+ List.fold_left
+ (fun (res,l,r) t ->
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ (demodulation_all_aux
+ metasenv context ugraph table lift_amount t),
+ l@[List.hd r], List.tl r)
+ (res, [], List.map (S.lift 1) l) l
+ in
+ res
+ | C.Prod (nn, s, t)
+ | C.Lambda (nn, s, t) ->
+ let context = (Some (nn, C.Decl s))::context in
+ let mk s t =
+ match term with
+ | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
+ in
+ res @
+ List.map
+ (fun (rel, subst, m, ug, c) ->
+ mk (S.lift 1 s) rel, subst, m, ug, c)
+ (demodulation_all_aux
+ metasenv context ugraph table (lift_amount+1) t)
+ (* we could demodulate also in s, but then t may be badly
+ * typed... *)
+ | t -> res
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let _, context, ugraph = env in
+ let solved goal res side =
+ let newg = build_newgoal bag context goal side Equality.Demodulation res in
+ match newg with
+ | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
+ when LibraryObjects.is_eq_URI uri ->
+ (try
+ let _ =
+ Founif.unification m m context left right CicUniv.empty_ugraph
+ in
+ Yes newg
+ with CicUnification.UnificationFailure _ -> No [newg])
+ | _ -> No [newg]
+ in
+ let solved goal res_list side =
+ let newg = List.map (fun x -> solved goal x side) res_list in
+ try
+ List.find (function Yes _ -> true | _ -> false) newg
+ with Not_found ->
+ No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+ in
+ let rec first f l =
+ match l with
+ | [] -> None
+ | x::tl ->
+ match f x with
+ | None -> first f tl
+ | Some x as ok -> ok
+ in
+ let rec aux steps next goal =
+ if steps = 0 then None else
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let do_step t =
+ demodulation_all_aux menv context ugraph table 0 t
+ in
+ match next with
+ | L ->
+ (match do_step left with
+ | _::_ as res ->
+ (match solved goal res Utils.Right with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> aux steps R goal)
+ | Yes newgoal -> Some newgoal)
+ | [] -> aux steps R goal)
+ | R ->
+ (match do_step right with
+ | _::_ as res ->
+ (match solved goal res Utils.Left with
+ | No newgoals ->
+ (match first (aux (steps - 1) L) newgoals with
+ | Some g as success -> success
+ | None -> None)
+ | Yes newgoal -> Some newgoal)
+ | [] -> None)
+ in
+ aux steps L initgoal
+;;
+
let get_stats () = "" ;;
Equality.equality_bag ->
Cic.context ->
Equality.equality -> string -> unit
+val solve_demodulating:
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal ->
+ int ->
+ Equality.goal option
+
(** profiling *)
val get_stats: unit -> string
ProofEngineTypes.goal list) option *
active_table * passive_table * int
-
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
let simpl = ReductionTactics.simpl_tac
+let solve_rewrite = Auto.solve_rewrite_tac
let split = IntroductionTactics.split_tac
let subst = SubstTactic.subst_tac
let symmetry = EqualityTactics.symmetry_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun 4 13:44:18 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 13 14:11:00 CEST 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val solve_rewrite :
+ universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val subst : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
shellglob)))
let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
+ let escape s = HSql.escape s in
let sql_pat = sqlpat_of_shellglob pat in
let query =
- sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
- "SELECT source FROM %s WHERE value LIKE \"%s\"")
- (MetadataTypes.name_tbl ()) sql_pat
- MetadataTypes.library_name_tbl sql_pat
+ sprintf
+ ("SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" "
+ ^^ "UNION " ^^
+ "SELECT source FROM %s WHERE value LIKE \"%s\" ESCAPE \"\\\" ")
+ (MetadataTypes.name_tbl ()) (escape sql_pat)
+ MetadataTypes.library_name_tbl (escape sql_pat)
in
let result = HSql.exec dbd query in
List.filter nonvar
in
String.concat "" (List.map aux script) ^ "\n\n"
-let txt_of_inline_macro style suri prefix =
+let txt_of_inline_macro ?map_unicode_to_tex style suri prefix =
let print_exc = function
| ProofEngineHelpers.Bad_pattern s as e ->
Printexc.to_string e ^ " " ^ Lazy.force s
let dbd = LibraryDb.instance () in
let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
let map uri =
- try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *)
- (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+ try
+ txt_of_cic_object
+ ?map_unicode_to_tex 78 style prefix
+ (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
with
| e ->
Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n"
val txt_of_cic_object:
?map_unicode_to_tex:bool ->
?skip_thm_and_qed:bool ->
- ?skip_initial_lambdas:bool ->
+ ?skip_initial_lambdas:int ->
int -> GrafiteAst.presentation_style -> string ->
Cic.obj ->
string
(* presentation_style, uri or baseuri, name prefix *)
val txt_of_inline_macro:
+ ?map_unicode_to_tex:bool ->
GrafiteAst.presentation_style -> string -> string -> string
in
let proof_script =
if List.exists (fun (s,_) -> s = "paramodulation") params then
- let proof_term =
+ let proof_term, how_many_lambdas =
Auto.lambda_close ~prefix_name:"orrible_hack_"
proof_term menv cc
in
ApplyTransformation.txt_of_cic_object
~map_unicode_to_tex:false
~skip_thm_and_qed:true
- ~skip_initial_lambdas:true
+ ~skip_initial_lambdas:how_many_lambdas
80 GrafiteAst.Declarative "" obj
else
if true then
cic2grafite cc menv proof_term
else
(* alternative using FG stuff *)
- let proof_term =
+ let proof_term, how_many_lambdas =
Auto.lambda_close ~prefix_name:"orrible_hack_"
proof_term menv cc
in
(ApplyTransformation.txt_of_cic_object
~map_unicode_to_tex:false
~skip_thm_and_qed:true
- ~skip_initial_lambdas:true
+ ~skip_initial_lambdas:how_many_lambdas
80 (GrafiteAst.Procedural None) "" obj))
in
let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
raise exn
(* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
| TA.Inline (_,style,suri,prefix) ->
- let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+ let str =
+ ApplyTransformation.txt_of_inline_macro
+ ~map_unicode_to_tex:false style suri prefix
+ in
[], str, String.length parsed_text
and eval_executable include_paths (buffer : GText.buffer) guistuff
projects / helm.git / commitdiff