From: Enrico Tassi Date: Tue, 7 Jun 2005 16:32:41 +0000 (+0000) Subject: added letin X-Git-Tag: PRE_INDEX_1~54 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15a4844b5d8f64a72964e5a917b6bd6d8d7dbe44;p=helm.git added letin --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 7471e4546..ae933d2d0 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -59,9 +59,10 @@ 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.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) -> @@ -183,6 +184,64 @@ let env_of_list l e = 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 @@ -276,6 +335,7 @@ let eval_command status cmd = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") in let metasenv = MatitaMisc.get_proof_metasenv status in + debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body); let (body_type, ugraph) = CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph in @@ -296,7 +356,8 @@ let eval_command status cmd = {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> command_error "The grammar should avoid having unnamed theorems!" - | TacticAst.Coercion (loc, term) -> assert false (** TODO *) + | TacticAst.Coercion (loc, coercion) -> + eval_coercion status coercion | TacticAst.Alias (loc, spec) -> match spec with | TacticAst.Ident_alias (id,uri) -> @@ -404,9 +465,11 @@ 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.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) @@ -567,7 +630,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 @@ -634,7 +699,6 @@ let initial_status = aliases = DisambiguateTypes.empty_environment; proof_status = No_proof; options = default_options (); - coercions = []; objects = []; }