From b173ec0accede3b3aba740d1e6c54ce9679bee9c Mon Sep 17 00:00:00 2001 From: bertot Date: Wed, 22 Jan 2003 17:18:05 +0000 Subject: removes all references to ctast.ml the Makefile has been updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3591 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/ascent.mli | 5 +- contrib/interface/centaur.ml4 | 17 ++- contrib/interface/dad.ml | 19 +-- contrib/interface/name_to_ast.ml | 12 +- contrib/interface/pbp.ml | 294 +-------------------------------------- contrib/interface/vtp.ml | 12 +- contrib/interface/xlate.ml | 145 +++++++------------ contrib/interface/xlate.mli | 3 - 8 files changed, 80 insertions(+), 427 deletions(-) (limited to 'contrib') diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index b62339fa5..a72963293 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -228,10 +228,11 @@ and ct_FORMULA = | CT_bang of ct_INT_OPT * ct_FORMULA | CT_cases of ct_FORMULA_OPT * ct_FORMULA_NE_LIST * ct_EQN_LIST | CT_cofixc of ct_ID * ct_COFIX_REC_LIST - | CT_elimc of ct_CASE * ct_FORMULA * ct_FORMULA * ct_FORMULA_LIST + | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST | CT_existvarc | CT_fixc of ct_ID * ct_FIX_BINDER_LIST | CT_if of ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA + | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA | CT_int_encapsulator of string | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA | CT_letin of ct_DEF * ct_FORMULA @@ -519,7 +520,7 @@ and ct_TACTIC_COM = | CT_split of ct_SPEC_LIST | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB | CT_symmetry - | CT_tac_double of ct_INT * ct_INT + | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 1a660a89f..fe25cb07d 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -37,7 +37,7 @@ open Translate;; open Name_to_ast;; open Pbp;; open Blast;; -open Dad;; +(* open Dad;; *) open Debug_tac;; open Search;; open Constrintern;; @@ -330,11 +330,13 @@ let globcv x = (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; +(* <\cpa> let pbp_tac_pcoq = pbp_tac (function (x:raw_tactic_expr) -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; + *) let blast_tac_pcoq = blast_tac (function (x:raw_tactic_expr) -> @@ -342,12 +344,13 @@ let blast_tac_pcoq = (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; - +(* <\cpa> let dad_tac_pcoq = dad_tac(function x -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; + *) let search_output_results () = output_results @@ -551,6 +554,9 @@ let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s) let pcoq_search s l = ctv_SEARCH_LIST:=[]; begin match s with + | SearchAbout locqid -> + raw_search_about (filter_by_module_from_list l) add_search + (Nametab.global locqid) | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in raw_pattern_search (filter_by_module_from_list l) add_search pat @@ -573,7 +579,7 @@ let pcoq_print_check j = let a,b = print_check j in output_results a b let pcoq_print_eval redfun env c j = - let strm, vtp = ct_print_eval (Ctast.ast_to_ct c) redfun env j in + let strm, vtp = ct_print_eval c redfun env j in output_results strm vtp;; open Vernacentries @@ -879,6 +885,7 @@ let command_creations = [ ];; *) +(* <\cpa> TACTIC EXTEND Pbp | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> [ if_pcoq pbp_tac_pcoq idopt nl ] @@ -891,6 +898,7 @@ TACTIC EXTEND Dad | [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] -> [ if_pcoq dad_tac_pcoq nl1 nl2 ] END + *) TACTIC EXTEND CtDebugTac | [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq t ] @@ -904,8 +912,9 @@ END let start_pcoq_mode debug = begin pcoq_started := Some debug; +(* <\cpa> start_dad(); - set_xlate_mut_stuff (fun x ->Ctast.ast_to_ct (globcv (Ctast.ct_to_ast x))); + *) declare_in_coq(); (* add_tactic "PcoqPbp" pbp_tac_pcoq; diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 00a4bb07e..4f03fb06f 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -11,7 +11,6 @@ open Tactics;; open Tacticals;; open Pattern;; open Reduction;; -open Ctast;; open Constrextern;; open Constrintern;; open Vernacinterp;; @@ -47,9 +46,7 @@ type dad_rule = constr_expr * int list * int list * int * int list * raw_atomic_tactic_expr;; -(* This value will be used systematically when constructing objects of - type Ctast.t, the value is stupid and meaningless, but it is needed - to construct well-typed terms. *) +(* This value will be used systematically when constructing objects *) let zz = (0,0);; @@ -70,17 +67,7 @@ let rec get_subterm (depth:int) (path: int list) (constr:constr) = first argument, an object of type env, is necessary to transform constr terms into abstract syntax trees. The second argument is the substitution, a list of pairs linking an integer and a constr term. *) -(* -let map_subst (env :env) - (subst:(int * Term.constr) list) = - let rec map_subst_aux = function - Coqast.Node(_, "META", [Coqast.Num(_, i)]) -> - let constr = List.assoc i subst in - ast_of_constr false env constr - | Coqast.Node(loc, s, l) -> Coqast.Node(loc, s, List.map map_subst_aux l) - | ast -> ast in - map_subst_aux;; -*) + let rec map_subst (env :env) (subst:(int * Term.constr) list) = function | CMeta (_,i) -> let constr = List.assoc i subst in @@ -274,7 +261,7 @@ let start_dad () = dad_status := true;; let add_dad_rule_fn name pat p1 p2 tac = let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in - add_dad_rule name (Ctast.ast_to_ct pat) p1 p2 (List.length pr) pr tac;; + add_dad_rule name pat p1 p2 (List.length pr) pr tac;; (* To be parsed by camlp4 diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 80009d783..039127cc5 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -155,17 +155,7 @@ let make_variable_ast name typ implicits = ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))])) ::(implicits_to_ast_list implicits);; -(* -let make_definition_ast name c typ implicits = - (ope("DEFINITION", - [string "DEFINITION"; - nvar name; - ope("COMMAND", - [ope("CAST", - [(constr_to_ast c); - (constr_to_ast (body_of_type typ))])])])):: - (implicits_to_ast_list implicits);; -*) + let make_definition_ast name c typ implicits = VernacDefinition (Global, name, DefineBody ([], None, (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index bc9f706c5..d4d134f64 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -7,7 +7,6 @@ open Tacticals;; open Hipattern;; open Pattern;; open Reduction;; -open Ctast;; open Rawterm;; open Environ;; @@ -88,34 +87,9 @@ type pbp_rule = (identifier list * identifier option -> (types, constr) kind_of_term -> int list -> pbp_sequence)) -> pbp_sequence option;; -(* -let make_named_intro s = - Node(zz, "Intros", - [Node(zz,"INTROPATTERN", - [Node(zz,"LISTPATTERN", - [Node(zz, "IDENTIFIER", - [Nvar(zz, s)])])])]);; -*) + let make_named_intro id = PbpIntros [id] -(* -let get_name_from_intro = function - Node(a, "Intros", - [Node(b,"INTROPATTERN", - [Node(c,"LISTPATTERN", - [Node(d, "IDENTIFIER", - [Nvar(e, s)])])])]) -> - Some s - | _ -> None;; -*) -(* -let make_clears = function - [] -> Node(zz, "Idtac",[]) - | str_list -> - Node(zz, "TRY", [Node(zz,"Clear", - [Node(zz, "CLAUSE", List.map (function s -> Nvar(zz,s)) str_list)]) - ]);; -*) let make_clears str_list = PbpThen [PbpTryClear str_list] let add_clear_names_if_necessary tactic clear_names = @@ -124,7 +98,6 @@ let add_clear_names_if_necessary tactic clear_names = | l -> chain_tactics [PbpTryClear l] tactic;; let make_final_cmd f optname clear_names constr path = -(* let tactic = f optname constr path in*) add_clear_names_if_necessary (f optname constr path) clear_names;; let (rem_cast:pbp_rule) = function @@ -336,23 +309,7 @@ let (not_intro: pbp_rule) = function -(* -let elim_with_bindings hyp_name names = - Node(zz,"Elim", - [Node(zz, "COMMAND", [Nvar(zz,hyp_name)]); - Node(zz,"BINDINGS", - List.map - (function s -> - Node(zz,"BINDING", - [Nvar(zz,s); - Node - (zz,"COMMAND", - [Node - (zz,"APPLIST", - [Nvar(zz,"PBP_META"); - Nvar(zz, - "value_for_" ^ s)])])])) names)]);; -*) + let elim_with_bindings hyp_name names = PbpElim (hyp_name, names);; @@ -448,114 +405,6 @@ let (mk_db_indices: int list -> int -> int list) = answer is true, then the built command takes advantage of the power of head tactics. *) -(* -let (head_tactic_patt: pbp_rule) = function - avoid, clear_names, clear_flag, Some h, cstr, path, f -> - (match down_prods (cstr, path, 0) with - | (str_list, _, nprems, - App(oper,[|c1|]), 2::1::path) - when - (is_matching_local (notconstr ()) oper) or - (is_matching_local (notTconstr ()) oper) -> - Some(Node(zz, "TACTICLIST", - [elim_with_bindings h str_list; - f avoid clear_names false None (kind_of_term c1) path])) - | (str_list, _, nprems, - App(oper, [|c1; c2|]), 2::a::path) - when ((is_matching_local (andconstr()) oper) or - (is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) -> - let h1 = next_global_ident_away (id_of_string "H") avoid in - let str_h1 = (string_of_id h1) in - let h2 = next_global_ident_away (id_of_string "H") (h1::avoid) in - let str_h2 = (string_of_id h2) in - Some(Node(zz,"TACTICLIST", - [elim_with_bindings h str_list; - make_named_intro str_h1; - make_named_intro str_h2; - let cont_body = - if a = 1 then c1 else c2 in - let cont_tac = - f (h2::h1::avoid) (h::clear_names) - false (Some (if 1 = a then str_h1 else str_h2)) - (kind_of_term cont_body) path in - if nprems = 0 then - cont_tac - else - Node(zz,"TACLIST", - cont_tac::(auxiliary_goals - clear_names clear_flag - h nprems))])) - | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path) - when ((is_matching_local (exconstr ()) oper) or - (is_matching_local (exTconstr ()) oper) or - (is_matching_local (sigconstr ()) oper) or - (is_matching_local (sigTconstr()) oper)) & a = 2 -> - (match (kind_of_term c2),path with - Lambda(Name x, _,body), (2::path) -> - Some(Node(zz,"TACTICLIST", - [elim_with_bindings h str_list; - let x' = next_global_ident_away x avoid in - let cont_body = - Prod(Name x', c1, - mkProd(Anonymous, body, - mkVar(dummy_id))) in - let cont_tac - = f avoid (h::clear_names) false None - cont_body (2::1::path) in - if nprems = 0 then - cont_tac - else - Node(zz,"TACLIST", - cont_tac::(auxiliary_goals - clear_names clear_flag - h nprems))])) - | _ -> None) - | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path) - when ((is_matching_local (orconstr ()) oper) or - (is_matching_local (sumboolconstr ()) oper) or - (is_matching_local (sumconstr ()) oper)) & - (a = 1 or a = 2) -> - Some(Node(zz, "TACTICLIST", - [elim_with_bindings h str_list; - let cont_body = - if a = 1 then c1 else c2 in - (* h' is the name for the new intro *) - let h' = next_global_ident_away (id_of_string "H") avoid in - let str_h' = (string_of_id h') in - let cont_tac = - Node(zz,"TACTICLIST", - [make_named_intro str_h'; - f - (* h' should not be used again *) - (h'::avoid) - (* the disjunct itself can be discarded *) - (h::clear_names) false (Some str_h') - (kind_of_term cont_body) path]) in - let snd_tac = - Node(zz, "TACTICLIST", - [make_named_intro str_h'; - make_clears (h::clear_names)]) in - let tacs1 = - if a = 1 then - [cont_tac; snd_tac] - else - [snd_tac; cont_tac] in - Node(zz,"TACLIST", - tacs1@(auxiliary_goals (h::clear_names) - false "dummy" nprems))])) - | (str_list, int_list, nprems, c, []) - when (check_apply c (mk_db_indices int_list nprems)) & - (match c with Prod(_,_,_) -> false - | _ -> true) & - (List.length int_list) + nprems > 0 -> - Some(add_clear_names_if_necessary - (Node(zz,"Apply", [Node(zz,"COMMAND",[Nvar(zz, h)]); - Node(zz,"BINDINGS", [])])) - clear_names) - | _ -> None) - | _ -> None;; -*) - let (head_tactic_patt: pbp_rule) = function avoid, clear_names, clear_flag, Some h, cstr, path, f -> (match down_prods (cstr, path, 0) with @@ -652,11 +501,6 @@ let pbp_rules = ref [rem_cast;head_tactic_patt;forall_intro;imply_intro2; and_intro; or_intro; not_intro; ex_intro];; -(* The tactic traced_try was intended to be used in tactics instead of - Try, with an argument Node(zz, "TACTIC", [b]) where b is the tactic to - try. However, the current design is not very robust to the fact that - Traced_Try may occur several times in the executed command! *) - let try_trace = ref true;; let traced_try (f1:tactic) g = @@ -670,24 +514,10 @@ let traced_try_entry = function | _ -> failwith "traced_try_entry received wrong arguments";; -let rec clean_trace flag = - function - Node(a,"Traced_Try", [Node(_,_,[b])]) -> - if flag then b else Node(zz,"Idtac",[]) - | Node(a,b,c) -> Node(a,b,List.map (clean_trace flag) c) - | t -> t;; - (* When the recursive descent along the path is over, one includes the command requested by the point-and-shoot strategy. Default is Try Assumption--Try Exact. *) -(* -let default_ast optname constr path = - match optname with - None -> Node(zz, "TRY", [Node(zz, "Assumption",[])]) - | Some(a) -> Node(zz, "TRY", - [Node(zz, "Exact",[Node(zz,"COMMAND",[Nvar(zz,a)])])]);; -*) let default_ast optname constr path = PbpThen [PbpTryAssumption optname] @@ -710,100 +540,12 @@ let rec pbpt final_cmd avoid clear_names clear_flag opt_name constr path = (* these are the optimisation functions. *) (* This function takes care of flattening successive then commands. *) -(* -let rec optim1 = - function - Node(a,"TACTICLIST",b) -> - let tacs = List.map optim1 b in - let rec flatten = function - | [Node(a, "TACTICLIST", b')] -> - let rec last = function - [] -> failwith "function last is called on an empty list" - | [b] -> b - | a::b -> last b in - (match last b' with - Node(a, "TACLIST",_) -> [Node(a,"TACTICLIST", b')] - | _ -> flatten b') - | Node(a, "TACTICLIST", b')::others -> List.append (flatten b') - (flatten others) - | Node(a, "Idtac",[])::others -> (flatten others) - | [Node(a, "TACLIST",tacs)] -> - [Node(a, "TACLIST", List.map optim1 tacs)] - | t1::others -> t1::(flatten others) - | [] -> [] in - (match (flatten tacs) with - [] -> Node(zz,"Idtac", []) - | [t] -> t - | args -> Node(zz,"TACTICLIST", args)) - | t -> t;; -*) (* Invariant: in [flatten_sequence t], occurrences of [PbpThenCont(l,t)] enjoy that t is some [PbpAtom t] *) -(* -let rec flatten_sequence = - function - PbpThens (tl1,tl2) -> PbpThens (tl1,List.map flatten_sequence tl2) - | PbpThen (tl1,t1) as x -> - (match flatten_sequence t1 with - | PbpThenCont (tl2,t2) -> PbpThenCont (tl1@tl2,t2) - | PbpThens (tl2,tl3) -> PbpThens (tl1@tl2,tl3) - | PbpAtom _ -> x) - | PbpAtom t as x -> x;; -*) (* This optimization function takes care of compacting successive Intro commands together. *) -(* -let rec optim2 = - function - Node(a,"TACTICLIST",b) -> - let get_ids = - List.map (function Node(_,"IDENTIFIER", [Nvar(_,s)])->s - | Node(_,s,_) -> (failwith "unexpected node " ^ s) - | _ -> failwith "get_ids expected an identifier") in - let put_ids ids = - Node(zz,"Intros", - [Node(zz,"INTROPATTERN", - [Node(zz,"LISTPATTERN", - List.map - (function s -> Node(zz,"IDENTIFIER",[Nvar(zz,s)])) - ids)])]) in - let rec group_intros names = function - [] -> (match names with - [] -> [] - | l -> [put_ids l]) - | Node(_,"Intros", - [Node(_,"INTROPATTERN",[Node(_,"LISTPATTERN", ids)])])::others -> - group_intros (names@(get_ids ids)) others - | [Node(a,"TACLIST",b')] -> - [Node(a,"TACLIST", List.map optim2 b')] - | t1::others -> - (match names with - [] -> t1::(group_intros [] others) - | l -> (put_ids l)::t1::(group_intros [] others)) in - Node(a,"TACTICLIST",group_intros [] b) - | t -> t;; -*) -(* -let rec optim2 = function - | TacThens (t,tl) -> TacThens (optim2 t, List.map optim2 tl) - | t -> - let get_ids = - List.map (function IntroIdentifier _ as x -> x - | _ -> failwith "get_ids expected an identifier") in - let rec group_intros names = function - [] -> (match names with - [] -> [] - | l -> [TacIntroPattern l]) - | (TacIntroPattern ids)::others -> - group_intros (names@(get_ids ids)) others - | t1::others -> - (match names with - [] -> t1::(group_intros [] others) - | l -> (TacIntroPattern l)::t1::(group_intros [] others)) in - make_then (group_intros [] (flatten_sequence t)) -*) let rec group_intros names = function [] -> (match names with @@ -819,37 +561,7 @@ let rec optim2 = function | PbpThens (tl1,tl2) -> PbpThens (group_intros [] tl1, List.map optim2 tl2) | PbpThen tl -> PbpThen (group_intros [] tl) -(* -let rec merge_ast_in_command com1 com2 = - let args1 = - (match com1 with - Node(_, "APPLIST", args) -> args - | _ -> failwith "unexpected com1 in merge_ast_in_command") in - let args2 = - (match com2 with - Node(_, "APPLIST", hyp::args) -> args - | _ -> failwith "unexpected com2 in merge_ast_in_command") in - Node(zz, "COMMAND", [Node(zz, "APPLIST", args1@args2)]);; -*) -(* -let cleanup_clears empty_allowed names str_list other = - let rec clean_aux = function - [] -> [] - | (Nvar(_,x) as fst_one)::tail -> - if List.mem x str_list then - clean_aux tail - else - fst_one::(clean_aux tail) - | _ -> failwith "unexpected argument in clean_aux" in - match clean_aux names with - [] -> (match other with - [] -> - if empty_allowed then - [] - else [Node(zz,"Idtac",[])] - | _ -> other) - | l -> Node(zz, "TRY", [Node(zz, "Clear", [Node(zz,"CLAUSE", l)])])::other;; -*) + let rec cleanup_clears str_list = function [] -> [] | x::tail -> diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 1a6bfc4ca..3e7cfd82a 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -590,7 +590,7 @@ and fFORMULA = function fNODE "cofixc" 2 | CT_elimc(x1, x2, x3, x4) -> fCASE x1; - fFORMULA x2; + fFORMULA_OPT x2; fFORMULA x3; fFORMULA_LIST x4; fNODE "elimc" 4 @@ -605,6 +605,12 @@ and fFORMULA = function fFORMULA x3; fFORMULA x4; fNODE "if" 4 +| CT_inductive_let(x1, x2, x3, x4) -> + fFORMULA_OPT x1; + fID_OPT_NE_LIST x2; + fFORMULA x3; + fFORMULA x4; + fNODE "inductive_let" 4 | CT_int_encapsulator x -> fATOM "int_encapsulator"; (f_atom_string x); print_string "\n"| CT_lambdac(x1, x2) -> @@ -1257,8 +1263,8 @@ and fTACTIC_COM = function fNODE "superauto" 4 | CT_symmetry -> fNODE "symmetry" 0 | CT_tac_double(x1, x2) -> - fINT x1; - fINT x2; + fID_OR_INT x1; + fID_OR_INT x2; fNODE "tac_double" 2 | CT_tacsolve(x,l) -> fTACTIC_COM x; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 3ac46fa7d..2e791e8d5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -5,7 +5,6 @@ open Char;; open Util;; open Ast;; open Names;; -open Ctast;; open Ascent;; open Genarg;; open Rawterm;; @@ -18,12 +17,6 @@ open Libnames;; let in_coq_ref = ref false;; -let xlate_mut_stuff = ref ((fun _ -> - Nvar((0,0), "function xlate_mut_stuff should not be used here")): - Ctast.t -> Ctast.t);; - -let set_xlate_mut_stuff v = xlate_mut_stuff := v;; - let declare_in_coq () = in_coq_ref:=true;; let in_coq () = !in_coq_ref;; @@ -168,18 +161,6 @@ let coerce_VARG_to_ID = x | _ -> xlate_error "coerce_VARG_to_ID";; -let xlate_id = - function - | Nvar (_, id) -> - (match id with - | "_" -> xlate_error "xlate_id: '_' is ident option" - | s -> CT_ident s) - | Id (_, id) -> - (match id with - | "_" -> xlate_error "xlate_id: '_' is ident option" - | s -> CT_ident s) - | _ -> xlate_error "xlate_id: not an identifier";; - let xlate_id_unit = function None -> CT_unit | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);; @@ -189,11 +170,6 @@ let xlate_ident_opt = | None -> ctv_ID_OPT_NONE | Some id -> ctf_ID_OPT_SOME (xlate_ident id) -let xlate_int = - function - | Num (_, n) -> CT_int n - | _ -> xlate_error "xlate_int: not an int";; - let xlate_id_to_id_or_int_opt s = CT_coerce_ID_OPT_to_ID_OR_INT_OPT (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));; @@ -210,11 +186,6 @@ let xlate_int_opt = function | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n) | None -> CT_coerce_NONE_to_INT_OPT CT_none -let xlate_string = - function - | Str (_, s) -> CT_string s - | _ -> xlate_error "xlate_string: not a string";; - let tac_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) @@ -240,16 +211,6 @@ let xlate_class = function | SortClass -> CT_ident "SORTCLASS" | RefClass qid -> loc_qualid_to_ct_ID qid -let split_params = - let rec sprec acc = - function - | (Id _ as p) :: l -> sprec (p::acc) l - | (Str _ as p) :: l -> sprec (p::acc) l - | (Num _ as p) :: l -> sprec (p::acc) l - | (Path _ as p) :: l -> sprec (p::acc) l - | l -> List.rev acc, l in - sprec [];; - let id_to_pattern_var ctid = match ctid with | CT_ident "_" -> @@ -261,14 +222,6 @@ let id_to_pattern_var ctid = exception Not_natural;; -let rec nat_to_number = - function - | Node (_, "APPLIST", ((Nvar (_, "S")) :: (v :: []) as v0)) -> - 1 + nat_to_number v - | Nvar (_, "O") -> 0 - | _ -> raise Not_natural;; - - let xlate_sort = function | RProp Term.Pos -> CT_sortc "Set" @@ -291,8 +244,9 @@ let xlate_reference = function let rec xlate_match_pattern = function | CPatAtom(_, Some s) -> id_to_pattern_var (xlate_reference s) - |CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_") - | CPatCstr (_, f1 , (arg1 :: args)) -> + | CPatAtom(_, None) -> id_to_pattern_var (CT_ident "_") + | CPatCstr(_, f, []) -> id_to_pattern_var (xlate_reference f) + | CPatCstr (_, f1 , (arg1 :: args)) -> CT_pattern_app (id_to_pattern_var (xlate_reference f1), CT_match_pattern_ne_list @@ -301,7 +255,9 @@ let rec xlate_match_pattern = | CPatAlias (_, pattern, id) -> CT_pattern_as (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id)) - | _ -> xlate_error "Unexpected data while translating a pattern";; + | CPatDelimiters(_, _, _) -> xlate_error "CPatDelimitors" + | CPatNumeral(_,_) -> xlate_error "CPatNumeral";; + @@ -340,6 +296,8 @@ and and xlate_binder_list = function l -> CT_binder_list( List.map xlate_binder_l l) +and cvt_fixpoint_binders bl = + CT_binder_list(List.map xlate_binder bl) and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function CRef r -> varc (xlate_reference r) @@ -361,19 +319,49 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> CT_if(xlate_formula_opt po, xlate_formula c,xlate_formula b1,xlate_formula b2) - + | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) -> + CT_inductive_let(xlate_formula_opt po, + xlate_id_opt_ne_list l, + xlate_formula c, xlate_formula b) + | COrderedCase (_,c,v,e,l) -> + let case_string = match c with + Term.MatchStyle -> "Match" + | _ -> "Case" in + CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e, + CT_formula_list(List.map xlate_formula l)) | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s) | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l) | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i) | CHole _ -> CT_existvarc - | COrderedCase (_,_,_,_,_) -> xlate_error "TODO:COrderedCase" | CDynamic (_, _) -> xlate_error "TODO:CDynamic" | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula num) - | CCast (_, _, _) -> xlate_error "TODO:CCast" - | CMeta (_, _) -> xlate_error "TODO:CMeta" - | CCoFix (_, _, _) -> xlate_error "TODO:CCoFix" - | CFix (_, _, _) -> xlate_error "TODO:CFix" - + | CCast (_, e, t) -> + CT_coerce_TYPED_FORMULA_to_FORMULA + (CT_typed_formula(xlate_formula e, xlate_formula t)) + | CMeta (_, i) -> CT_coerce_ID_to_FORMULA(CT_metac (CT_int i)) + | CCoFix (_, (_, id), lm::lmi) -> + let strip_mutcorec (fid, arf, ardef) = + CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in + CT_cofixc(xlate_ident id, + (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))) + | CFix (_, (_, id), lm::lmi) -> + let strip_mutrec (fid, n, arf, ardef) = + let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in + let arf = xlate_formula arf in + let ardef = xlate_formula ardef in + match cvt_fixpoint_binders bl with + | CT_binder_list (b :: bl) -> + CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl), + arf, ardef) + | _ -> xlate_error "mutual recursive" in + CT_fixc (xlate_ident id, + CT_fix_binder_list + (CT_coerce_FIX_REC_to_FIX_BINDER + (strip_mutrec lm), List.map + (fun x-> CT_coerce_FIX_REC_to_FIX_BINDER (strip_mutrec x)) + lmi)) + | CCoFix _ -> assert false + | CFix _ -> assert false and xlate_formula_expl = function (a, None) -> xlate_formula a | (a, i) -> CT_bang(xlate_int_opt i, xlate_formula a) @@ -519,17 +507,6 @@ let is_tactic_special_case = function "AutoRewrite" -> true | _ -> false;; -let tactic_special_case cont_function cvt_arg = function - "AutoRewrite", (tac::v::bl) -> - CT_autorewrite - (CT_id_ne_list(xlate_id v, List.map xlate_id bl), - CT_coerce_TACTIC_COM_to_TACTIC_OPT(cont_function tac)) - | "AutoRewrite", (v::bl) -> - CT_autorewrite - (CT_id_ne_list(xlate_id v, List.map xlate_id bl), - CT_coerce_NONE_to_TACTIC_OPT CT_none) - | _ -> assert false;; - let xlate_context_pattern = function | Term v -> CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v) @@ -703,9 +680,8 @@ and xlate_tac = | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b) | TacChange (_, f, b) -> xlate_error "TODO: Change subterms" | TacExtend (_,"Contradiction",[]) -> CT_contradiction - | TacDoubleInduction (AnonHyp n1, AnonHyp n2) -> - CT_tac_double (CT_int n1, CT_int n2) - | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2" + | TacDoubleInduction (n1, n2) -> + CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2) | TacExtend (_,"Discriminate", [idopt]) -> CT_discriminate_eq (xlate_quantified_hypothesis_opt @@ -1146,30 +1122,6 @@ let build_record_field_list l = xlate_error "TODO: manifest fields in Record" in CT_recconstr_list (List.map build_record_field l);; -let xlate_ast = - let rec xlate_ast_aux = - function - | Node (_, s, tl) -> - CT_astnode (CT_ident s, CT_ast_list (List.map xlate_ast_aux tl)) - | Nvar (_, s) -> - CT_coerce_ID_OR_STRING_to_AST - (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) - | Slam (_, (Some s), t) -> - CT_astslam (CT_coerce_ID_to_ID_OPT (CT_ident s), xlate_ast_aux t) - | Slam (_, None, t) -> CT_astslam (ctv_ID_OPT_NONE, xlate_ast_aux t) - | Num (_, i) -> failwith "Numbers not treated in xlate_ast" - | Id (_, s) -> - CT_coerce_ID_OR_STRING_to_AST - (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) - | Str (_, s) -> - CT_coerce_ID_OR_STRING_to_AST - (CT_coerce_STRING_to_ID_OR_STRING (CT_string s)) - | Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast" - | Path (_, sl) -> - CT_astpath - (CT_id_list (List.map (function s -> CT_ident s) sl)) in - xlate_ast_aux;; - let get_require_flags impexp spec = let ct_impexp = match impexp with @@ -1198,8 +1150,7 @@ let cvt_vernac_binder = function let cvt_vernac_binders args = CT_binder_list(List.map cvt_vernac_binder args) -let cvt_fixpoint_binders bl = - CT_binder_list(List.map xlate_binder bl) + let xlate_comment = function CommentConstr c -> CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula c) diff --git a/contrib/interface/xlate.mli b/contrib/interface/xlate.mli index 6109816b5..bedb4ac82 100644 --- a/contrib/interface/xlate.mli +++ b/contrib/interface/xlate.mli @@ -3,10 +3,7 @@ open Ascent;; val xlate_vernac : Vernacexpr.vernac_expr -> ct_COMMAND;; val xlate_tactic : Tacexpr.raw_tactic_expr -> ct_TACTIC_COM;; val xlate_formula : Topconstr.constr_expr -> ct_FORMULA;; -val xlate_int : Ctast.t -> ct_INT;; -val xlate_string : Ctast.t -> ct_STRING;; val xlate_ident : Names.identifier -> ct_ID;; val xlate_vernac_list : Vernacexpr.vernac_expr -> ct_COMMAND_LIST;; -val set_xlate_mut_stuff : (Ctast.t -> Ctast.t) -> unit;; val declare_in_coq : (unit -> unit);; -- cgit v1.2.3