X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=7471e4546e7db2c5841bc1ea2d85884ea910c444;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=7e7ac5641e3ea71b3b2c42f854d9455e0375f192;hpb=4faa2b8428b153e5e80c758880236178399fa0fe;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 7e7ac5641..7471e4546 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,12 @@ 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 @@ -56,9 +60,60 @@ let tactic_of_ast = function | 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.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 @@ -103,6 +158,31 @@ 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_command status cmd = match cmd with | TacticAst.Set (loc, name, value) -> set_option status name value @@ -132,6 +212,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 @@ -154,7 +239,25 @@ let eval_command status cmd = MatitaSync.add_inductive_def ~uri ~types ~params:[] ~leftno ~ugraph status in - {status with proof_status = No_proof } + (* 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") @@ -185,9 +288,14 @@ let eval_command status cmd = let body = CicMetaSubst.apply_subst subst body in let ty = CicMetaSubst.apply_subst subst ty in 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!" + command_error "The grammar should avoid having unnamed theorems!" | TacticAst.Coercion (loc, term) -> assert false (** TODO *) | TacticAst.Alias (loc, spec) -> match spec with @@ -297,9 +405,25 @@ let disambiguate_tactic status = function | 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.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) @@ -482,12 +606,14 @@ let eval_ast status ast = (* 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 =