X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=148f550fdcee8f3946d949f32e5bca86e605c193;hb=53ee2f5095adadffcafb40e436d23dc330d3bd87;hp=7e7ac5641e3ea71b3b2c42f854d9455e0375f192;hpb=4faa2b8428b153e5e80c758880236178399fa0fe;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 7e7ac5641..148f550fd 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -1,8 +1,9 @@ open Printf - open MatitaTypes +let debug = false ;; +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 @@ -45,7 +50,7 @@ let tactic_of_ast = function | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what | TacticAst.Auto (_,num) -> - AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ()) + AutoTactic.auto_tac ~num (MatitaDb.instance ()) | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what (* (* TODO Zack a lot more of tactics to be implemented here ... *) @@ -55,10 +60,64 @@ 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 +162,71 @@ let eval_tactical status tac = in apply_tactic (tactical_of_ast tac) +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 @@ -133,10 +257,15 @@ let eval_command status cmd = MatitaLog.message (sprintf "%s defined" suri); let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in {status with proof_status = No_proof } + | TacticAst.Record (loc, params, name, ty, fields) -> + let suri = MatitaMisc.qualify status name ^ ".ind" in + let record_spec = (suri, params, ty, fields) in + let status = MatitaSync.add_record_def record_spec status 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 - * semantic content is the len, that is leftno (note: leftno and pamaters - * have nothing in common). + * semantic content is the len, that is leftno (note: leftno and + * paramaters have nothing in common). *) let suri = match types with @@ -151,10 +280,9 @@ let eval_command status cmd = (types, [], leftno) CicUniv.empty_ugraph in let status = - MatitaSync.add_inductive_def - ~uri ~types ~params:[] ~leftno ~ugraph status + MatitaSync.add_inductive_def ~uri ~types ~leftno ~ugraph status in - {status with proof_status = No_proof } + {status with proof_status = No_proof } | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") @@ -180,15 +308,17 @@ 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 {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) -> @@ -249,7 +379,7 @@ let disambiguate_term status term = in status, cic -let disambiguate_terms status terms = +let disambiguate_closedtypes status terms = let term = CicAst.pack terms in let status, term = disambiguate_term status term in status, CicUtil.unpack term @@ -296,10 +426,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) @@ -380,7 +528,7 @@ let disambiguate_inddef status params indTypes = add_ast (add_pi params typ); List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) indTypes; - let status, terms = disambiguate_terms status !asts in + let status, terms = disambiguate_closedtypes status !asts in let terms = ref (List.rev terms) in let get_term () = match !terms with [] -> assert false | hd :: tl -> terms := tl; hd @@ -418,7 +566,41 @@ let disambiguate_inddef status params indTypes = let cicIndTypes = List.rev cicIndTypes in status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) +let disambiguate_record status params ty fields = + let packed = + List.fold_right + (fun (name,ast) acc -> + CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) + (params @ ["",ty] @ fields) (CicAst.Sort `Type) + in + debug_print (CicAstPp.pp_term packed); + let status, packed = disambiguate_term status packed in + let rec split t = function + | [] -> [],t + | (n,_)::tl -> + match t with + | Cic.Prod (_, src, tgt) -> + let l, t = split tgt tl in + (n, src) :: l, t + | _-> assert false + in + let params, t = split packed params in + let ty, t = + match t with + | Cic.Prod (_ , ty, t) -> ty, t + | _ -> assert false + in + let fields, _ = + split (let t,_,_ = CicMetaSubst.delift_rels [] [] 1 t in t) fields + in + params, ty, fields + let disambiguate_command status = function + | TacticAst.Record(loc, params,name,ty,fields) -> + let params, ty, fields = + disambiguate_record status params ty fields + in + status, TacticAst.Record(loc, params, name, ty, fields) | TacticAst.Inductive (loc, params, types) -> let (status, (uri, (ind_types, vars, paramsno))) = disambiguate_inddef status params types @@ -443,7 +625,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 +641,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 +665,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 +693,7 @@ let initial_status = aliases = DisambiguateTypes.empty_environment; proof_status = No_proof; options = default_options (); - coercions = []; objects = []; } +