X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaEngine.ml;h=8aae7633a9222fd8f8dc86b0a3d737369827492b;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=7e7ac5641e3ea71b3b2c42f854d9455e0375f192;hpb=4faa2b8428b153e5e80c758880236178399fa0fe;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 7e7ac5641..8aae7633a 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 @@ -55,10 +60,62 @@ 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.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 @@ -103,6 +160,96 @@ 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 context = [] in + let src_uri = + let ty_src = CicReduction.whd context ty_src in + UriManager.uri_of_string (CicUtil.uri_of_term ty_src) + in + let tgt_uri = + let ty_tgt = CicReduction.whd context ty_tgt in + 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 @@ -132,6 +279,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 +306,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") @@ -180,15 +350,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 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) -> @@ -296,10 +473,28 @@ 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.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) @@ -443,7 +638,9 @@ 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 @@ -457,9 +654,8 @@ let disambiguate_executable status ex = let status, cmd = disambiguate_command status cmd in status, (TacticAst.Command (loc, cmd)) | TacticAst.Macro (_, mac) -> - command_error - (sprintf ("The engine is not allowed to disambiguate any macro, "^^ - "in particular %s") (TacticAstPp.pp_macro_ast mac)) + command_error (sprintf "The macro %s can't be in a script" + (TacticAstPp.pp_macro_ast mac)) let disambiguate_comment status c = match c with @@ -482,12 +678,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 = @@ -508,7 +706,6 @@ let initial_status = aliases = DisambiguateTypes.empty_environment; proof_status = No_proof; options = default_options (); - coercions = []; objects = []; }