X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=3c141126d3c26f8c80be266fc8e18588c42016b4;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=59d1c7b79891464d51348e9136716dadd4fd5303;hpb=716da638633f01d6a5b52c05e0bd6adc86385b60;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 59d1c7b79..3c141126d 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -1,8 +1,9 @@ open Printf - open MatitaTypes +let debug = true ;; +let debug_print = if debug then prerr_endline else ignore ;; (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation @@ -19,9 +20,13 @@ let namer_of names = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ let tactic_of_ast = function - | TacticAst.Intros (_, _, names) -> + | TacticAst.Intros (_, None, names) -> (* TODO Zack implement intros length *) PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () + | TacticAst.Intros (_, Some num, names) -> + (* TODO Zack implement intros length *) + PrimitiveTactics.intros_tac ~howmany:num + ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Reflexivity _ -> Tactics.reflexivity | TacticAst.Assumption _ -> Tactics.assumption | TacticAst.Contradiction _ -> Tactics.contradiction @@ -40,7 +45,8 @@ let tactic_of_ast = function | TacticAst.Cut (_, term) -> Tactics.cut term | TacticAst.Elim (_, term, _) -> (* TODO Zack implement "using" argument *) - Tactics.elim_intros_simpl term + (* old: Tactics.elim_intros_simpl term *) + Tactics.elim_intros term | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what | TacticAst.Auto (_,num) -> @@ -54,11 +60,67 @@ let tactic_of_ast = function | TacticAst.Discriminate of 'ident | TacticAst.Fold of reduction_kind * 'term | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option *) + | TacticAst.LetIn (loc,term,name) -> + Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name]) + | TacticAst.ReduceAt (_,reduction_kind,ident,path) -> + ProofEngineTypes.mk_tactic + (fun (((_,metasenv,_,_),goal) as status) -> + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let where, also_in_hypotheses = + if ident = "goal" then + ty, false + else + let hyp = + try + List.find (function + | Some (Cic.Name name,entry) when name = ident -> true + | _ -> false) + context + with + Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis")) + in + (match hyp with + | Some (_, Cic.Decl term) -> term + | Some (_, Cic.Def (term,ty)) -> term + | None -> assert false),true + in + let pointers = CicUtil.select ~term:where ~context:path in + (match reduction_kind with + | `Normalize -> + ProofEngineTypes.apply_tactic + (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Reduce -> + ProofEngineTypes.apply_tactic + (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Simpl -> + ProofEngineTypes.apply_tactic + (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers)) + status + | `Whd -> + ProofEngineTypes.apply_tactic + (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers)) + status)) + | TacticAst.Reduce (_,reduction_kind,opts) -> + let terms, also_in_hypotheses = + match opts with + | Some (l,`Goal) -> Some l, false + | Some (l,`Everywhere) -> Some l, true + | None -> None, false + in + (match reduction_kind with + | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms + | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms + | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms + | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) + | TacticAst.Rewrite (_,dir,t,ident) -> + if dir = `Left then + EqualityTactics.rewrite_tac ~term:t + else + EqualityTactics.rewrite_back_tac ~term:t | _ -> assert false let eval_tactical status tac = @@ -98,6 +160,89 @@ let eval_tactical status tac = in apply_tactic (tactical_of_ast tac) +(** given a uri and a type list (the contructors types) builds a list of pairs + * (name,uri) that is used to generate authomatic aliases **) +let extract_alias types uri = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + ((name, UriManager.string_of_uriref (uri,[i])) + :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) + ) (acc,1) cl))),i+1 + ) ([],0) types) + +(** adds a (name,uri) list l to a disambiguation environment e **) +let env_of_list l e = + let module DT = DisambiguateTypes in + let module DTE = DisambiguateTypes.Environment in + List.fold_left ( + fun e (name,uri) -> + DTE.add + (DT.Id name) + (uri,fun _ _ _ -> CicUtil.term_of_uri uri) + e + ) e l + +let eval_coercion status coercion = + let coer_uri,coer_ty = + match coercion with + | Cic.Const (uri,_) + | Cic.Var (uri,_) -> + let o,_ = + CicEnvironment.get_obj CicUniv.empty_ugraph uri + in + (match o with + | Cic.Constant (_,_,ty,_,_) + | Cic.Variable (_,_,ty,_,_) -> + uri,ty + | _ -> assert false) + | Cic.MutConstruct (uri,t,c,_) -> + let o,_ = + CicEnvironment.get_obj CicUniv.empty_ugraph uri + in + (match o with + | Cic.InductiveDefinition (l,_,_,_) -> + let (_,_,_,cl) = List.nth l t in + let (_,cty) = List.nth cl c in + uri,cty + | _ -> assert false) + | _ -> assert false + in + (* we have to get the source and the tgt type uri + * in Coq syntax we have already their names, but + * since we don't support Funclass and similar I think + * all the coercion should be of the form + * (A:?)(B:?)T1->T2 + * So we should be able to extract them from the coercion type + *) + let extract_last_two_p ty = + let rec aux = function + | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2)) + | Cic.Prod( _, src, tgt) -> src, tgt + | _ -> assert false + in + aux ty + in + let ty_src,ty_tgt = extract_last_two_p coer_ty in + let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in + let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in + let new_coercions = + (* also adds them to the Db *) + CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri + in + let status = + List.fold_left ( + fun s (uri,o,ugraph) -> + match o with + | Cic.Constant (_,Some body, ty, params, attrs) -> + MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status + | _ -> assert false + ) status new_coercions + in + {status with proof_status = No_proof} + let eval_command status cmd = match cmd with | TacticAst.Set (loc, name, value) -> set_option status name value @@ -127,6 +272,11 @@ let eval_command status cmd = "type you've declared!"); MatitaLog.message (sprintf "%s defined" suri); let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in + let status = + let name = UriManager.name_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + {status with aliases = new_env } + in {status with proof_status = No_proof } | TacticAst.Inductive (loc, dummy_params, types) -> (* dummy_params are not real params, it is a list of nothing, and the only @@ -145,8 +295,29 @@ let eval_command status cmd = CicTypeChecker.typecheck_mutual_inductive_defs uri (types, [], leftno) CicUniv.empty_ugraph in + let status = MatitaSync.add_inductive_def - ~uri ~types ~params:[] ~leftno ~ugraph status; + ~uri ~types ~params:[] ~leftno ~ugraph status + in + (* aliases for the constructors and types *) + let aliases = env_of_list (extract_alias types uri) status.aliases in + (* aliases for the eliminations principles *) + let aliases = + let base = String.sub suri 0 (String.length suri - 4) in + env_of_list + (List.fold_left ( + fun acc suffix -> + if List.exists ( + fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix + ) status.objects then + let u = base ^ suffix in + (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc + else + acc + ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases + in + let status = {status with proof_status = No_proof } in + { status with aliases = aliases} | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") @@ -172,14 +343,22 @@ let eval_command status cmd = CicUnification.fo_unif metasenv [] body_type ty ugraph in if metasenv <> [] then - command_error - "metasenv not empty while giving a definition with body"; + command_error ( + "metasenv not empty while giving a definition with body: " ^ + CicMetaSubst.ppmetasenv metasenv []) ; let body = CicMetaSubst.apply_subst subst body in let ty = CicMetaSubst.apply_subst subst ty in - MatitaSync.add_constant ~uri ~body ~ty ~ugraph status + let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in + let status = + let suri = UriManager.string_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + {status with aliases = new_env } + in + {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> - command_error "The grammas should avoid having unnamed theorems!" - | TacticAst.Coercion (loc, term) -> assert false (** TODO *) + command_error "The grammar should avoid having unnamed theorems!" + | TacticAst.Coercion (loc, coercion) -> + eval_coercion status coercion | TacticAst.Alias (loc, spec) -> match spec with | TacticAst.Ident_alias (id,uri) -> @@ -200,14 +379,21 @@ let eval_command status cmd = (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } -let eval status st = - match st with +let eval_executable status ex = + match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac | TacticAst.Command (_, cmd) -> eval_command status cmd | TacticAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" (TacticAstPp.pp_macro_cic mac)) +let eval_comment status c = status + +let eval status st = + match st with + | TacticAst.Executable (_,ex) -> eval_executable status ex + | TacticAst.Comment (_,c) -> eval_comment status c + let disambiguate_term status term = let (aliases, metasenv, cic, _) = match @@ -280,11 +466,31 @@ let disambiguate_tactic status = function | TacticAst.Discriminate of 'ident | TacticAst.Fold of reduction_kind * 'term | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option *) + | TacticAst.LetIn (loc,term,name) -> + let status, term = disambiguate_term status term in + status, TacticAst.LetIn (loc,term,name) + | TacticAst.ReduceAt (loc, reduction_kind, ident, path) -> + let path = Disambiguate.interpretate [] status.aliases path in + status, TacticAst.ReduceAt(loc, reduction_kind, ident, path) + | TacticAst.Reduce (loc, reduction_kind, opts) -> + let status, opts = + match opts with + | None -> status, None + | Some (l,pat) -> + let status, l = + List.fold_right (fun t (status,acc) -> + let status',t' = disambiguate_term status t in + status', t'::acc) + l (status,[]) + in + status, Some (l, pat) + in + status, TacticAst.Reduce (loc, reduction_kind, opts) + | TacticAst.Rewrite (loc,dir,t,ident) -> + let status, term = disambiguate_term status t in + status, TacticAst.Rewrite (loc,dir,term,ident) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) @@ -425,13 +631,15 @@ let disambiguate_command status = function status, Some body in status, TacticAst.Theorem (loc, thm_flavour, name, ty, body) - | TacticAst.Coercion (loc, term) -> assert false (** TODO *) + | TacticAst.Coercion (loc, term) -> + let status, term = disambiguate_term status term in + status, TacticAst.Coercion (loc,term) | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> status, cmd | TacticAst.Alias _ as x -> status, x -let disambiguate_statement status statement = - match statement with +let disambiguate_executable status ex = + match ex with | TacticAst.Tactical (loc, tac) -> let status, tac = disambiguate_tactical status tac in status, (TacticAst.Tactical (loc, tac)) @@ -442,18 +650,36 @@ let disambiguate_statement status statement = command_error (sprintf ("The engine is not allowed to disambiguate any macro, "^^ "in particular %s") (TacticAstPp.pp_macro_ast mac)) + +let disambiguate_comment status c = + match c with + | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n) + | TacticAst.Code (loc,ex) -> + let status, ex = disambiguate_executable status ex in + status, TacticAst.Code (loc,ex) + +let disambiguate_statement status statement = + match statement with + | TacticAst.Comment (loc,c) -> + let status, c = disambiguate_comment status c in + status, TacticAst.Comment (loc,c) + | TacticAst.Executable (loc,ex) -> + let status, ex = disambiguate_executable status ex in + status, TacticAst.Executable (loc,ex) let eval_ast status ast = let status,st = disambiguate_statement status ast in (* this disambiguation step should be deferred to support tacticals *) eval status st -let eval_from_stream status str = - let st = CicTextualParser2.parse_statement str in - eval_ast status st +let eval_from_stream status str cb = + let stl = CicTextualParser2.parse_statements str in + List.fold_left + (fun status ast -> cb status ast;eval_ast status ast) status + stl let eval_string status str = - eval_from_stream status (Stream.of_string str) + eval_from_stream status (Stream.of_string str) (fun _ _ -> ()) let default_options () = let options = @@ -474,7 +700,6 @@ let initial_status = aliases = DisambiguateTypes.empty_environment; proof_status = No_proof; options = default_options (); - coercions = []; objects = []; }