diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/eterm.ml | 30 | ||||
| -rw-r--r-- | contrib/subtac/infer.ml | 827 | ||||
| -rw-r--r-- | contrib/subtac/infer.mli | 59 | ||||
| -rw-r--r-- | contrib/subtac/interp.ml | 661 | ||||
| -rw-r--r-- | contrib/subtac/natural.ml | 10 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.ml | 682 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.mli | 3 | ||||
| -rw-r--r-- | contrib/subtac/sast.ml | 25 | ||||
| -rw-r--r-- | contrib/subtac/scoq.ml | 7 | ||||
| -rw-r--r-- | contrib/subtac/sparser.ml4 | 168 | ||||
| -rw-r--r-- | contrib/subtac/sutils.ml | 11 | ||||
| -rw-r--r-- | contrib/subtac/sutils.mli | 3 |
12 files changed, 690 insertions, 1796 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 7b07abbc8..e59dead34 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -7,10 +7,23 @@ open Term open Names -open Sutils open Evd open List open Pp + +(** Utilities to find indices in lists *) +let list_index x l = + let rec aux i = function + k :: tl -> if k = x then i else aux (succ i) tl + | [] -> raise Not_found + in aux 0 l + +let list_assoc_index x l = + let rec aux i = function + (k, v) :: tl -> if k = x then i else aux (succ i) tl + | [] -> raise Not_found + in aux 0 l + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) let subst_evars evs n t = @@ -91,28 +104,19 @@ let eterm evm t = in - let declare_evar (id, c) = + let _declare_evar (id, c) = let id = id_of_string ("Evar" ^ string_of_int id) in ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c, Decl_kinds.IsAssumption Decl_kinds.Definitional)) in - let declare_assert acc (id, c) = + let _declare_assert acc (id, c) = let id = id_of_string ("Evar" ^ string_of_int id) in tclTHEN acc (Tactics.assert_tac false (Name id) c) in msgnl (str "Term constructed in Eterm" ++ Termops.print_constr_env (Global.env ()) t''); Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts) - (* t'' *) - (* Hack: push evars as assumptions in the global env *) -(* iter declare_evar evts; *) -(* Tactics.apply t' *) - (*tclTHEN (fold_left declare_assert tclIDTAC evts) (Tactics.apply t')*) open Tacmach -let etermtac (evm, t) = - let t' = eterm evm t in - t' -(* Tactics.apply (Reduction.nf_betaiota t') - Tactics.exact (Reduction.nf_betaiota t')*) +let etermtac (evm, t) = eterm evm t diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml deleted file mode 100644 index d52d8edf5..000000000 --- a/contrib/subtac/infer.ml +++ /dev/null @@ -1,827 +0,0 @@ -open Natural -open Names -open Term -open Rawterm -open Util -open Sast -open Scoq -open Pp -open Printer - -let ($) f g = fun x -> f (g x) - -let app_option f default = function Some x -> f x | None -> default - -let concat_map f l = - let rec aux accu = function - [] -> List.rev accu - | hd :: tl -> - aux (f hd @ accu) tl - in aux [] l - -let unique l = - let l' = List.sort Pervasives.compare l in - let rec aux accu = function - [] -> List.rev accu - | x :: (y :: _) as tl when x = y -> - aux accu tl - | hd :: tl -> - aux (hd :: accu) tl - in aux [] l' - -type term_pp = Pp.std_ppcmds - -type subtyping_error = - | UncoercibleInferType of loc * term_pp * term_pp - | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp - -type typing_error = - | NonFunctionalApp of loc * term_pp * term_pp - | NonConvertible of loc * term_pp * term_pp - | NonSigma of loc * term_pp - -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error - -exception Debug_msg of string - -let typing_error e = raise (Typing_error e) -let subtyping_error e = raise (Subtyping_error e) - -type sort = Term.sorts -type sort_loc = sort located - -(* Decorated terms *) -type dterm = - DRel of nat - | DLambda of (name located * dtype_loc) * dterm_loc * dtype_loc - | DApp of dterm_loc * dterm_loc * dtype_loc - | DLetIn of (name located) * dterm_loc * dterm_loc * dtype_loc - | DLetTuple of (name located * dtype_loc * dtype_loc) list * dterm_loc * dterm_loc * dtype_loc - | DIfThenElse of dterm_loc * dterm_loc * dterm_loc * dtype_loc - | DSum of ((name located) * dterm_loc) * (dterm_loc * dtype_loc) * dtype_loc - | DCoq of constr * dtype_loc -and dterm_loc = dterm located -and dtype = - | DTApp of dtype_loc * dtype_loc * dtype_loc * sort_loc - | DTPi of (name located * dtype_loc) * dtype_loc * sort_loc - | DTSigma of (name located * dtype_loc) * dtype_loc * sort_loc - | DTSubset of (identifier located * dtype_loc) * dtype_loc * sort_loc - | DTRel of nat - | DTTerm of dterm_loc * dtype_loc * sort_loc - | DTSort of sort_loc - | DTInd of (identifier located) * dtype_loc * inductive * sort_loc - | DTCoq of types * dtype_loc * sort_loc -and dtype_loc = dtype located - -let print_name = function - Name s -> str (string_of_id s) - | Anonymous -> str "_" - -let print_name_loc (_, n) = print_name n - -let string_of_list l = - let rec aux = function - hd :: ((_ :: _) as tl) -> - hd ++ str "," ++ aux tl - | hd :: [] -> hd - | [] -> mt() - in aux l - -type context = (name * dtype_loc) list - -let print_dtype_locref : (context -> dtype_loc -> std_ppcmds) ref = - ref (fun ctx t -> mt()) - -let print_context ctx = - let cmds, _ = - List.fold_right - (fun (x, t) (acc, ctx) -> - let xpr = print_name x ++ str " : " ++ !print_dtype_locref ctx t in - (xpr :: acc), ((x, t) :: ctx)) - ctx ([], []) - in string_of_list cmds - -let type_of_rel ctx n = - try snd (List.nth ctx n) - with e -> - debug 3 (str "Error in type_of_rel, searching for index " ++ str (string_of_int n) - ++ str " in context " ++ print_context ctx ++ str ": " ++ - str (Printexc.to_string e)); - raise e - -let name_of_rel ctx n = - try fst (List.nth ctx n) - with e -> - debug 3 (str "Error in name_of_rel, searching for index " ++ str (string_of_int n) - ++ str " in context " ++ print_context ctx ++ str ": " ++ - str (Printexc.to_string e)); - raise e - -let rec sort_of_dtype ctx = function - | DTApp (_, _, _, x) - | DTPi (_, _, x) - | DTSigma (_, _, x) - | DTSubset (_, _, x) - | DTTerm (_, _, x) - | DTSort x - | DTInd (_, _, _, x) - | DTCoq (_, _, x) -> x - | DTRel i -> sort_of_dtype_loc ctx (type_of_rel ctx i) - -and sort_of_dtype_loc ctx (_, t) = sort_of_dtype ctx t - -let rec no_var n (loc, t) = - match t with - | DTApp (x, y, t, _) -> (no_var n x) && (no_var n y) - | DTPi ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) - | DTSigma ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) - | DTSubset ((_, x), y, _) -> (no_var n x) && (no_var (succ n) y) - | DTRel i when i <> n -> false - | x -> true - - -let rec lift_rec n k (loc, t) = - let t' = - match t with - | DTApp (x, y, t, s) -> DTApp (lift_rec n k x, lift_rec n k y, - lift_rec n k t, s) - | DTPi ((id, x), y, s) -> - DTPi ((id, lift_rec n k x), lift_rec n (succ k) y, s) - | DTSigma ((id, x), y, s) -> - DTSigma ((id, lift_rec n k x), lift_rec n (succ k) y, s) - | DTSubset ((id, x), y, s) -> - DTSubset ((id, lift_rec n k x), lift_rec n (succ k) y, s) - | (DTRel i) as x -> - if i < k then x else DTRel (n + i) - | DTTerm (t, tt, s) -> DTTerm (lift_term_rec n k t, lift_rec n k tt, s) - | DTCoq (c, t, s) -> DTCoq (Term.liftn n k c, lift_rec n k t, s) - | DTSort _ - | DTInd _ -> t - in loc, t' - -and lift_term_rec n k (loc, s) = - let s' = - match s with - DRel i -> - if i < k then s else DRel (n + i) - | DLambda ((nl, dt), dt', dtlam) -> - DLambda ((nl, lift_rec n k dt), lift_term_rec n (succ k) dt', - lift_rec n k dtlam) - | DApp (dte, dte', dt) -> - DApp (lift_term_rec n k dte, lift_term_rec n k dte', lift_rec n k dt) - | DLetIn (nl, dte, dte', dt) -> - DLetIn (nl, lift_term_rec n k dte, lift_term_rec n (succ k) dte', - lift_rec n k dt) - | DLetTuple (nl, dte, dte', dt) -> - DLetTuple (nl, lift_term_rec n k dte, - lift_term_rec n (List.length nl + k) dte', - lift_rec n k dt) - | DIfThenElse (db, de, de', dt) -> - DIfThenElse (lift_term_rec n k db, lift_term_rec n k de, - lift_term_rec n k de', lift_rec n k dt) - | DSum ((x, tx), (ty, dty), dt) -> - DSum ((x, lift_term_rec n k tx), - (lift_term_rec n (succ k) ty, lift_rec n (succ k) dty), - lift_rec n k dt) - | DCoq (c, t) -> DCoq (Term.liftn n k c, lift_rec n k t) - in loc, s' - -let lift n t = lift_rec n 0 t -let lift_term n t = lift_term_rec n 0 t - -let rec unlift_rec n k (loc, t) = - let t' = - match t with - | DTApp (x, y, t, s) -> DTApp (unlift_rec n k x, unlift_rec n k y, unlift_rec n k t, s) - | DTPi ((id, x), y, s) -> - DTPi ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) - | DTSigma ((id, x), y, s) -> - DTSigma ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) - | DTSubset ((id, x), y, s) -> - DTSubset ((id, unlift_rec n k x), unlift_rec n (succ k) y, s) - | (DTRel i) as x -> - if i < k then x else DTRel (i - n) - | DTTerm (t, tt, s) -> DTTerm (unlift_term_rec n k t, unlift_rec n k tt, s) - | DTCoq (c, t, s) -> DTCoq (c, unlift_rec n k t, s) - | DTSort _ - | DTInd _ -> t - in loc, t' - -and unlift_term_rec n k (loc, s) = - let s' = - match s with - DRel i -> - if i < k then s else DRel (i - n) - | DLambda ((nl, dt), dt', dtlam) -> - DLambda ((nl, unlift_rec n k dt), unlift_term_rec n (succ k) dt', - unlift_rec n k dtlam) - | DApp (dte, dte', dt) -> - DApp (unlift_term_rec n k dte, unlift_term_rec n k dte', unlift_rec n k dt) - | DLetIn (nl, dte, dte', dt) -> - DLetIn (nl, unlift_term_rec n k dte, unlift_term_rec n (succ k) dte', - unlift_rec n k dt) - | DLetTuple (nl, dte, dte', dt) -> - DLetTuple (nl, unlift_term_rec n k dte, - unlift_term_rec n (List.length nl + k) dte', - unlift_rec n k dt) - | DIfThenElse (db, de, de', dt) -> - DIfThenElse (unlift_term_rec n k db, unlift_term_rec n k de, - unlift_term_rec n k de', unlift_rec n k dt) - | DSum ((x, tx), (ty, dty), dt) -> - DSum ((x, unlift_term_rec n k tx), - (unlift_term_rec n k ty, unlift_rec n k dty), - unlift_rec n k dt) - | DCoq (c, t) -> DCoq (c, unlift_rec n k t) - in loc, s' - -let unlift n t = unlift_rec n 0 t - -let rec type_of_dterm ctx t = - match t with - DRel (i) -> - (try let t = type_of_rel ctx i in lift (succ i) t - with e -> debug 3 (str "Couldn't find type of rel in type_of_dterm"); - raise e) - | DLambda (_, _, dt) -> dt - | DApp (dte, dte', dt) -> dt - | DLetIn (nl, dte, dte', dt) -> dt - | DLetTuple (nl, dte, dte', dt) -> dt - | DIfThenElse (db, de, de', dt) -> dt - | DSum (_, _, dt) -> dt - | DCoq (_, dt) -> dt - -let type_of_dterm_loc ctx (_, t) = type_of_dterm ctx t - -let rec subst_term_type_rec (loc, s) t k = - let s' = - match s with - DRel i -> - if k < i then DRel (pred i) - else if k = i then - match snd (lift_rec k 0 t) with - DTRel i -> DRel i - | DTTerm (t, _, _) -> snd t - | _ -> failwith ("Substitution of a type in a term") - else (* k > i *) s - | DLambda ((ln, dt), e, t') -> - DLambda ((ln, subst_rec dt t k), subst_term_type_rec e t (succ k), - subst_rec t' t k) - | DApp (x, y, ta) -> - DApp (subst_term_type_rec x t k, subst_term_type_rec y t k, subst_rec ta t k) - | DLetIn (nl, e, e', t') -> - DLetIn (nl, subst_term_type_rec e t k, subst_term_type_rec e' t (succ k), - subst_rec t' t k) - | DLetTuple (nl, e, e', t') -> - DLetTuple (nl, subst_term_type_rec e t k, subst_term_type_rec e' t (k + List.length nl), - subst_rec t' t k) - | DIfThenElse (b, e, e', t') -> - DIfThenElse (subst_term_type_rec b t k, subst_term_type_rec e t k, - subst_term_type_rec e' t k, subst_rec t' t k) - | DSum ((nl, dt), (dt', tt'), t') -> - DSum ((nl, subst_term_type_rec dt t k), - (subst_term_type_rec dt' t (succ k), subst_rec tt' t (succ k)), - subst_rec t' t k) - | DCoq (c, dt) -> DCoq (c, subst_rec dt t k) - in loc, s' - -and subst_term_rec (loc, s) t k = - let ttype = - let dtype = type_of_dterm [] (snd t) in - (dummy_loc, (DTTerm (t, dtype, sort_of_dtype_loc [] dtype))) - in - let s' = - match s with - DRel i -> - if k < i then DRel (pred i) - else if k = i then snd (lift_term_rec k 0 t) - else (* k > i *) s - | DLambda ((ln, dt), e, t') -> - (* !!! *) - DLambda ((ln, subst_rec dt ttype k), - subst_term_rec e t (succ k), subst_rec t' ttype k) - | DApp (x, y, ta) -> - DApp (subst_term_rec x t k, subst_term_rec y t k, subst_rec ta ttype k) - | DLetIn (nl, e, e', t') -> - DLetIn (nl, subst_term_rec e t k, subst_term_rec e' t (succ k), - subst_rec t' ttype k) - | DLetTuple (nl, e, e', t') -> - DLetTuple (nl, subst_term_rec e t k, subst_term_rec e' t - (k + List.length nl), - subst_rec t' ttype k) - | DIfThenElse (b, e, e', t') -> - DIfThenElse (subst_term_rec b t k, subst_term_rec e t k, - subst_term_rec e' t k, subst_rec t' ttype k) - | DSum ((nl, dt), (dt', tt'), t') -> - DSum ((nl, subst_term_rec dt t k), - (subst_term_rec dt' t (succ k), subst_rec tt' tt' (succ k)), - subst_rec t' ttype k) - | DCoq (c, dt) -> - - DCoq (c, subst_rec dt ttype k) - in loc, s' - -and subst_rec (loc, s) (t : dtype_loc) k = - let s' = - match s with - DTPi ((id, a), b, s) -> DTPi ((id, subst_rec a t k), - subst_rec b t (succ k), s) - | DTSigma ((id, a), b, s) -> DTSigma ((id, subst_rec a t k), - subst_rec b t (succ k), s) - | DTSubset ((id, a), b, s) -> DTSubset ((id, subst_rec a t k), - subst_rec b t (succ k), s) - | DTRel i -> - if k < i then DTRel (pred i) - else if k = i then snd (lift k t) - else (* k > i *) s - | DTApp (x, y, t', s) -> DTApp (subst_rec x t k, subst_rec y t k, - subst_rec t' t k, s) - | DTTerm (x, tt, s) -> DTTerm (subst_term_type_rec x t k, subst_rec tt t k, s) - | DTCoq (c, ct, s) -> DTCoq (c, subst_rec ct t k, s) - | DTSort _ | DTInd _ -> s - in loc, s' - -let subst s t = subst_rec s t 0 -let subst_term s t = subst_term_rec s t 0 - -let rec print_dterm' ctx = function - | DRel n -> - (try - print_name (name_of_rel ctx n) ++ str ("(" ^ (string_of_int n) ^ ")") - with Failure _ -> str ("UNBOUND_REL_" ^ (string_of_int n))) - | DLambda ((namel, t), e, _) -> str "fun " ++ print_name (snd namel) ++ spc () ++ - str ":" ++ spc () ++ print_dtype' ctx (snd t) ++ spc () ++ str "=>" ++ spc () - ++ print_dterm_loc ((snd namel, t) :: ctx) e - | DApp (x, y, _) -> (print_dterm_loc ctx x) ++ spc () ++ - str "(" ++ (print_dterm_loc ctx y) ++ str ")" - | DLetIn (n, e, e', _) -> - let te = - try type_of_dterm_loc ctx e - with e -> debug 3 (str "Couldn't find type_of_dterm in print_dterm'"); - raise e - in - str "let" ++ spc () ++ print_name_loc n - ++ spc () ++ str "=" ++ spc () ++ print_dterm_loc ctx e ++ - print_dterm_loc ((snd n, te) :: ctx) e' - | DLetTuple (nl, t, e, _) -> - str "let" ++ spc () ++ str "(" ++ - string_of_list (List.rev_map (fun (n, _, _) -> print_name_loc n) nl) - ++ str ")" ++ spc () ++ str "=" ++ spc () ++ - print_dterm_loc ctx t ++ str "in" ++ spc () ++ - print_dterm_loc ((List.map (fun (x, y, z) -> (snd x, y)) nl) @ ctx) e - | DIfThenElse (b, t, t', _) -> - let ctx' = (Name (id_of_string "H"), (dummy_loc, DTRel 0)) :: ctx in - str "if" ++ spc () ++ print_dterm_loc ctx b ++ spc () ++ - str "then" ++ spc () ++ print_dterm_loc ctx' t ++ spc () ++ - str "else" ++ spc () ++ print_dterm_loc ctx' t' - | DSum ((n, t), (t', tt'), _) -> - let ctx' = - try (snd n, type_of_dterm_loc ctx t) :: ctx - with e -> debug 3 (str "Couldn't find type_of_dterm in print_dterm' (sum)"); - raise e - in - str "(" ++ print_name (snd n) ++ str ":=" - ++ print_dterm_loc ctx t ++ str "," - ++ print_dterm_loc ctx' t' ++ str ":" - ++ print_dtype_loc ctx' tt' ++ str ")" - | DCoq (cstr, t) -> pr_constr cstr - -and print_dterm_loc ctx (_, x) = print_dterm' ctx x - (*debug_msg 1 (str ":" ++ print_dtype_loc ctx (type_of_dterm ctx x))*) - -and print_dtype' ctx = function - | DTApp (x, y, t, s) -> print_dtype_loc ctx x ++ spc() ++ - str "(" ++ print_dtype_loc ctx y ++ str ")" - | DTPi ((id, x), y, s) -> - str "(" ++ print_name_loc id ++ str ":" ++ print_dtype_loc ctx x ++ str ")" - ++ spc() ++ print_dtype_loc ((snd id, x) :: ctx) y - | DTSigma ((id, x), y, s) -> - str "[" ++ print_name_loc id ++ str ":" ++ print_dtype_loc ctx x ++ str "]" - ++ spc() ++ print_dtype_loc ((snd id, x) :: ctx) y - | DTSubset ((id, x), y, s) -> - str "{" ++ str (string_of_id (snd id)) ++ str ":" ++ print_dtype_loc ctx x ++ str "|" - ++ spc() ++ print_dtype_loc ((Name (snd id), x) :: ctx) y ++ str "}" - | (DTRel i) as x -> - (try print_name (name_of_rel ctx i) ++ str ("(" ^ (string_of_int i) ^ ")") - with Failure _ -> str ("_UNBOUND_REL_" ^ (string_of_int i))) - | DTTerm (t, tt, s) -> str "Term:(" ++ print_dterm_loc ctx t ++ str ")" - | DTInd (n, t, i, s) -> str (string_of_id (snd n)) - | DTCoq (c, t, s) -> - debug_msg 1 (str "Coq:(") ++ pr_constr c ++ - debug_msg 1 (str ":" ++ print_dtype_loc ctx t ++ str ")") - | DTSort s -> - pr_constr (mkSort (snd s)) - -and print_dtype_loc ctx (_, t) = print_dtype' ctx t - -let _ = print_dtype_locref := print_dtype_loc - -let rec reduce_term t = - match t with - | DLambda ((n, x), y, dt) -> DLambda ((n, reduce_type_loc x), reduce_term_loc y, reduce_type_loc dt) - | DApp (dte, dte', dt) -> snd (subst_term dte' dte) - | DLetIn (nl, dte, dte', dt) -> snd (subst_term dte' dte) - | DLetTuple (nl, dte, dte', dt) -> t (* TODO *) - | DIfThenElse (db, de, de', dt) -> t (* TODO *) - | DSum _ | DRel _ | DCoq _ -> t - -and reduce_term_loc (loc, t) = (loc, reduce_term t) - -and reduce_type = function - | DTApp (x, y, t, s) -> snd (subst y x) - | DTPi ((id, x), y, s) -> DTPi ((id, reduce_type_loc x), reduce_type_loc y, s) - | DTSigma ((id, x), y, s) -> DTSigma ((id, reduce_type_loc x), reduce_type_loc y, s) - | DTSubset ((id, x), y, s) -> DTSubset ((id, reduce_type_loc x), reduce_type_loc y, s) - | (DTRel i) as x -> x - | DTTerm (t, tt, s) -> DTTerm (reduce_term_loc t, reduce_type_loc tt, s) - | DTInd (n, t, i, s) as x -> x - | DTCoq (c, t, s) as x -> x - | DTSort _ as x -> x - -and reduce_type_loc (loc, t) = (loc, reduce_type t) - - -let rec type_equiv ctx u v = - trace (str "Check type equivalence: " ++ print_dtype_loc ctx u ++ str " and " ++ print_dtype_loc ctx v); - match snd u, snd v with - DTCoq (_, x, _), y -> type_equiv ctx x v - | x, DTCoq (_, y, _) -> type_equiv ctx u y - - | DTApp (_, _, t, _), _ -> type_equiv ctx t v - | _, DTApp (_, _, t, _) -> type_equiv ctx u t - - | (DTPi ((_, x), y, _), DTPi ((n', x'), y', _)) -> - type_equiv ctx x x' && type_equiv ((snd n', x') :: ctx) y y' - | (DTSigma ((_, x), y, _), DTSigma ((n', x'), y', _)) -> - type_equiv ctx x x' && type_equiv ((snd n', x') :: ctx) y y' - | (DTSubset ((_, x), y, _), DTSubset ((_, x'), y', _)) -> - type_equiv ctx x x' - | (DTRel x, DTRel y) -> x = y - | (DTInd (n, _, i, _), DTInd (n', _, i', _)) -> i == i' || i = i' - | _ -> false - -let convertible ctx u v = - type_equiv ctx (reduce_type_loc u) (reduce_type_loc v) - -let rec check_subtype ctx u v = - trace (str "Check subtype: " ++ print_dtype_loc ctx u ++ str " and " ++ print_dtype_loc ctx v); - match (snd u, snd v) with - DTCoq (_, t, _), _ -> check_subtype ctx t v - | _, DTCoq (_, t, _) -> check_subtype ctx u t - - | DTInd (_, t, _, _), _ -> check_subtype ctx t v - | _, DTInd (_, t, _, _) -> check_subtype ctx u t - - | DTApp (_, _, t, _), _ -> check_subtype ctx t v - | _, DTApp (_, _, t, _) -> check_subtype ctx u t - - | DTRel i, _ -> - let t = - try type_of_rel ctx i - with e -> - debug 3 (str "Couldn't find type_of_rel in check_subtype"); - raise e - in check_subtype ctx (lift (succ i) t) v - | _, DTRel i -> - let t = - try type_of_rel ctx i - with e -> debug 3 (str "Couldn't find type_of_rel in check_subtype"); - raise e - in - check_subtype ctx u (lift (succ i) t) - - | (DTPi ((_, x), y, _), DTPi ((n', x'), y', _)) -> - check_subtype ctx x' x && check_subtype ((snd n', x') :: ctx) y y' - - | (DTSigma ((_, x), y, _), DTSigma ((n', x'), y', _)) -> - check_subtype ctx x x' && check_subtype ((snd n', x') :: ctx) y y' - - | (DTSubset ((_, x), y, _), _) -> check_subtype ctx x v - | (_, DTSubset ((_, x), y, _)) -> check_subtype ctx u x - | (DTSort s, DTSort s') -> - (match snd s, snd s' with - Prop _, Type _ -> true - | x, y -> x = y) - | _ -> convertible ctx u v - -let rec mu ctx = function - | DTSubset ((_, x), y, _) -> mu ctx (snd x) - | DTCoq (_, x, _) -> mu ctx (snd x) - | DTInd (_, t, _, _) -> mu ctx (snd t) - | DTApp (_, _, t, _) -> mu ctx (snd t) - | DTRel i -> mu ctx (snd (type_of_rel ctx i)) - | x -> x - -exception Not_implemented of string - -let notimpl s = raise (Not_implemented s) - -let type_application ctx ((locx, x) as tx) ((locy, y) as ty) = - let narg, targ, tres, sres = - match mu ctx x with - | DTPi ((n, x), y, z) -> n, x, y, z - | x -> - typing_error (NonFunctionalApp (locx, - (print_dtype_loc ctx tx), - (print_dtype' ctx x))) - in - try - if check_subtype ctx ty targ then - let dtres = subst tres ty in - debug 1 (str "Subst of " ++ print_dtype_loc ctx ty ++ str " in " ++ - print_dtype_loc ((snd narg, targ) :: ctx) tres); - debug 1 (str "Subst in result type: " ++ print_dtype_loc ctx dtres); - dummy_loc, DTApp (tx, ty, dtres, sort_of_dtype_loc ctx dtres) - else - subtyping_error (UncoercibleInferType - (locy, print_dtype_loc ctx ty, print_dtype_loc ctx targ)) - - with e -> raise e (* Todo check exception etc.. *) - - -let rec dtype_of_types ctx c = - let dt = - match kind_of_term c with - | Rel i -> - DTRel (pred i) - | Var id -> - let ref = Nametab.locate (Libnames.make_short_qualid id) in - let t = Libnames.constr_of_global ref in - snd (dtype_of_types ctx t) - | Meta mv -> notimpl "Meta" - | Evar pex -> notimpl "Evar" - | Sort s -> DTSort (dummy_loc, s) - | Cast (c, _, t) -> snd (dtype_of_types ctx t) - | Prod (n, t, t') -> - let dt = dtype_of_types ctx t in - let ctx' = (n, dt) :: ctx in - let dt' = dtype_of_types ctx' t' in - DTPi (((dummy_loc, n), dt), dt', sort_of_dtype_loc ctx' dt') - | Lambda (n, t, e) -> notimpl "Lambda" - | LetIn (n, e, t, e') -> notimpl "LetIn" - | App (f, el) -> - snd (List.fold_left - (fun acc el -> - let tel = dtype_of_types ctx el in - type_application ctx acc tel) - (dtype_of_types ctx f) (Array.to_list el)) - | Const cst -> - let t = Global.lookup_constant cst in - let dt = dtype_of_types ctx t.Declarations.const_type in - DTCoq (c, dt, sort_of_dtype_loc ctx dt) - | Ind i -> - let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in - DTInd ((dummy_loc, ind.Declarations.mind_typename), - dtype_of_types ctx ind.Declarations.mind_nf_arity, - i, (dummy_loc, ind.Declarations.mind_sort)) - (* let t = Inductiveops.type_of_inductive (Global.env ()) i in *) -(* debug "Lookup inductive"; *) - (* let dt = dtype_of_types ctx t in *) -(* DTCoq (t, dt, sort_of_dtype_loc ctx dt) *) - - | Construct con -> - let t = Inductiveops.type_of_constructor (Global.env ()) con in - let dt = dtype_of_types ctx t in - DTCoq (c, dt, sort_of_dtype_loc ctx dt) - | Case _ -> notimpl "Case" - | Fix fixpt -> notimpl "Fixpoint" - | CoFix cofixpt -> notimpl "CoFixpoint" - in dummy_loc, dt - -let rec dtype_of_constr ctx c = - let dt = - match kind_of_term c with - | Rel i -> DTRel (pred i) - | Var id -> - let ref = Nametab.locate (Libnames.make_short_qualid id) in - let t = Libnames.constr_of_global ref in - snd (dtype_of_constr ctx t) - | Meta mv -> notimpl "Meta" - | Evar pex -> notimpl "Evar" - | Sort s -> DTSort (dummy_loc, s) - | Cast (_,_,t) -> snd (dtype_of_constr ctx t) - | Prod (n, t, t') -> - let dt = dtype_of_constr ctx t in - let ctx' = (n, dt) :: ctx in - let dt' = dtype_of_constr ctx' t' in - DTPi (((dummy_loc, n), dt), dt', sort_of_dtype_loc ctx' dt') - | Lambda (n, t, e) -> notimpl "Lambda" - | LetIn (n, e, t, e') -> notimpl "LetIn" - | App (f, el) -> - snd (List.fold_left - (fun acc el -> - type_application ctx acc (dtype_of_constr ctx el)) - (dtype_of_constr ctx f) (Array.to_list el)) - | Const cst -> - let t = Global.lookup_constant cst in - let dt = dtype_of_constr ctx t.Declarations.const_type in - snd dt - - | Ind i -> - let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in - DTInd ((dummy_loc, ind.Declarations.mind_typename), - dtype_of_types ctx ind.Declarations.mind_nf_arity, - i, (dummy_loc, ind.Declarations.mind_sort)) - - | Construct con -> - let t = Inductiveops.type_of_constructor (Global.env ()) con in - let dt = dtype_of_constr ctx t in - snd dt - | Case _ -> notimpl "Case" - | Fix fixpt -> notimpl "Fixpoint" - | CoFix cofixpt -> notimpl "CoFixpoint" - in dummy_loc, dt - -let list_assoc_index x l = - let rec aux i = function - (y, _) :: tl -> if x = y then i else aux (succ i) tl - | [] -> debug 2 (str "raising not_found in list_assoc_index"); - raise Not_found - in aux 0 l - -let coqref ctx (loc, r) = - let qualid = Libnames.make_short_qualid r in - try - let gr = Nametab.locate qualid in - debug 3 (str "Resolved " ++ str (string_of_id r) ++ str " globally"); - Libnames.constr_of_global gr - with Not_found -> - debug 3 (str "Error in coqref"); - Nametab.error_global_not_found_loc loc qualid - -let coqtermref ctx r = - let constr = coqref ctx r in - let dtype = dtype_of_constr ctx constr in - DCoq (constr, dtype), dtype - -let coqtyperef ctx r = - let constr = coqref ctx r in - let dtype = dtype_of_types ctx constr in - snd dtype, dtype - -let debug_loc n (loc, e) = - debug n (Toplevel.print_toplevel_error (Stdpp.Exc_located (loc, Debug_msg e))) - -let rec dtype n ctx (loc, t) = - let t' = - match t with - TApp (x, y) -> - let tx, ty = dtype n ctx x, dtype n ctx y in - snd (type_application ctx tx ty) - | TPi ((name, t), t') -> - let dt = dtype n ctx t in - let dt' = dtype (succ n) ((snd name, dt) :: ctx) t' in - DTPi ((name, dt), dt', (dummy_loc, type_0)) - | TSigma ((name, t), t') -> - let dt = dtype n ctx t in - let dt' = dtype (succ n) ((snd name, dt) :: ctx) t' in - DTSigma ((name, dt), dt', (dummy_loc, type_0)) - | TSubset ((i, t), t') -> - let dt = dtype n ctx t in - let ctx' = (Name (snd i), dt) :: ctx in - let dt' = dtype (succ n) ctx' t' in - DTSubset ((i, dt), dt', sort_of_dtype_loc ctx dt) - | TIdent (loc, i) -> - let name = Name i in - if List.mem_assoc name ctx then - let typ = List.assoc name ctx in - let index = list_assoc_index name ctx in - debug 3 (str "Resolved " ++ str (string_of_id i) ++ str " locally"); - DTRel index - else fst (coqtyperef ctx (loc, i)) - | TTerm t -> let t, tt = dterm n ctx t in DTTerm (t, tt, sort_of_dtype_loc ctx tt) - in (loc, t') - -and dterm n ctx (loc, t) = - let t', tt' = - match t with - | SIdent li -> - begin - let name = Name (snd li) in - if List.mem_assoc name ctx then - let typ = List.assoc name ctx in - let index = list_assoc_index name ctx in - let typ' = lift (succ index) typ in - debug 3 (str "Resolved " ++ str (string_of_id (snd li)) ++ str " locally"); - DRel index, typ' - else coqtermref ctx li - end - - | SLambda (((loc, name) as ln, t), e) -> - let dt = dtype n ctx t in - let name = Name name in - let ln = loc, name in - let ctx' = (name, dt) :: ctx in - let de, te = dterm (succ n) ctx' e in - let dpi = dummy_loc, DTPi ((ln, dt), te, sort_of_dtype_loc ctx' te) in - DLambda ((ln, dt), de, dpi), dpi - - | SLetIn ((loc, name) as ln, e, e') -> - let de, te = dterm n ctx e in - let de', te' = dterm (succ n) ((name, te) :: ctx) e' in - DLetIn (ln, de, de', te'), te' - - | SApp (f, e) -> - let dt, tf = dterm n ctx f in - let narg, targ, tres, sres = - match mu ctx (snd tf) with - | DTPi ((n, x), y, z) -> n, x, y, z - | x -> typing_error (NonFunctionalApp - (fst f, print_dterm_loc ctx dt, - print_dtype' ctx x)) - in - let de, te = dterm n ctx e in - (try - if check_subtype ctx te targ then - let term = (dummy_loc, DTTerm (de, te, sort_of_dtype_loc ctx te)) in - let dtres = subst tres term in - debug 1 (str "Subst of " ++ print_dtype_loc ctx term ++ str " in " ++ - print_dtype_loc ((snd narg, targ) :: ctx) tres); - debug 1 (str "Subst in result type: " ++ print_dtype_loc ctx dtres); - DApp (dt, de, dtres), dtres - else - subtyping_error - (UncoercibleInferTerm (fst e, - print_dtype_loc ctx te, - print_dtype_loc ctx targ, - print_dterm_loc ctx de, - print_dterm_loc ctx dt)) - - - with e -> raise e (* Todo check exception etc.. *)) - - | SSumDep (((loc, id), t), (t', tt')) -> - let dt, tt = dterm n ctx t in - let ctx' = (Name id, tt) :: ctx in - let tt' = dtype (succ n) ctx' tt' in - let dt', _ = dterm (succ n) ctx' t' in - let rest = dummy_loc, - DTSigma (((loc, Name id), tt), tt', sort_of_dtype_loc ctx' tt') - in - DSum (((loc, Name id), dt), (dt', tt'), rest), rest - - | SSumInf (t, t') -> - let dt, tt = dterm n ctx t in - let ctx' = (Anonymous, tt) :: ctx in - let dt', tt' = dterm (succ n) ctx' t' in - let rest = dummy_loc, - DTSigma (((dummy_loc, Anonymous), tt), tt', sort_of_dtype_loc ctx' tt') - in - DSum (((dummy_loc, Anonymous), dt), (dt', tt'), rest), rest - - | SIfThenElse (b, t, t') -> - let dn, tn = dterm n ctx b in - let ctx' = (Name (id_of_string "H"), - (dummy_loc, - DTCoq (Term.mkVar (id_of_string "H"), - (dummy_loc, DTSort (dummy_loc, mk_Set)), - (dummy_loc, type_0)))) :: ctx - in - let dt, tt = dterm (succ n) ctx' t - and dt', tt' = dterm (succ n) ctx' t' in - if convertible ctx' tt tt' then - DIfThenElse (dn, dt, dt', tt), (unlift 1 tt) - else typing_error (NonConvertible (loc, print_dtype_loc ctx' tt, - print_dtype_loc ctx' tt')) - - | SLetTuple (nl, t, t') -> - let dt, tt = dterm n ctx t in - debug 2 (str "Let tuple e type: " ++ print_dtype_loc ctx tt); - let rec aux n lctx tt l = - match snd tt, l with - DTSigma ((nl, t), t', s), nl' :: ((_ :: _) as tl) -> - aux (succ n) ((nl', t, tt) :: lctx) t' tl - | _, [nl] -> - (nl, tt, tt) :: lctx - | _, _ -> typing_error (NonSigma (fst tt, print_dtype_loc ctx tt)) - in - let ctx' = aux 0 [] tt nl in - let ctx'' = (List.map (fun (nl, t, t') -> (snd nl, t)) ctx') @ ctx in - let dt', tt' = dterm ((List.length nl) + n) ctx'' t' in - let t = DLetTuple (ctx', dt, dt', unlift (List.length nl) tt') in - debug 2 (str "Parsed let-tuple: " ++ print_dterm' ctx t); - debug 2 (str "ctx' = "); - debug 2 (str "ctx' = " ++ - let cmds, _ = - (List.fold_right - (fun (x, t, t') (acc, ctx) -> - let acc' = print_name_loc x ++ str ":" ++ - print_dtype_loc ctx t - in - let ctx' = (snd x, t) :: ctx in - (acc ++ spc () ++ acc', ctx')) - ctx' (mt (), ctx)) - in cmds); - - debug 2 (str "Parsed let-tuple in-term: " ++ print_dterm_loc ctx'' dt'); - debug 2 (str "Parsed let-tuple type: " ++ - print_dtype_loc ((List.map (fun (x, t, _) -> snd x, t) ctx') @ ctx) tt'); - t, tt' - - - in (loc, t'), tt' - -let infer ctx t = dterm 0 ctx t -let infer_type ctx t = dtype 0 ctx t - diff --git a/contrib/subtac/infer.mli b/contrib/subtac/infer.mli deleted file mode 100644 index 637e9edb1..000000000 --- a/contrib/subtac/infer.mli +++ /dev/null @@ -1,59 +0,0 @@ -type term_pp = Pp.std_ppcmds - -type subtyping_error = - | UncoercibleInferType of Util.loc * term_pp * term_pp - | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp - -type typing_error = - | NonFunctionalApp of Util.loc * term_pp * term_pp - | NonConvertible of Util.loc * term_pp * term_pp - | NonSigma of Util.loc * term_pp - -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error -exception Debug_msg of string - -val subtyping_error : subtyping_error -> 'a -val typing_error : typing_error -> 'a - -type sort = Term.sorts -type sort_loc = sort Util.located -type dterm = - DRel of Natural.nat - | DLambda of (Names.name Util.located * dtype_loc) * dterm_loc * dtype_loc - | DApp of dterm_loc * dterm_loc * dtype_loc - | DLetIn of Names.name Util.located * dterm_loc * dterm_loc * dtype_loc - | DLetTuple of (Names.name Util.located * dtype_loc * dtype_loc) list * - dterm_loc * dterm_loc * dtype_loc - | DIfThenElse of dterm_loc * dterm_loc * dterm_loc * dtype_loc - | DSum of (Names.name Util.located * dterm_loc) * (dterm_loc * dtype_loc) * - dtype_loc - | DCoq of Term.constr * dtype_loc -and dterm_loc = dterm Util.located -and dtype = - DTApp of dtype_loc * dtype_loc * dtype_loc * sort_loc - | DTPi of (Names.name Util.located * dtype_loc) * dtype_loc * sort_loc - | DTSigma of (Names.name Util.located * dtype_loc) * dtype_loc * sort_loc - | DTSubset of (Names.identifier Util.located * dtype_loc) * dtype_loc * - sort_loc - | DTRel of Natural.nat - | DTTerm of dterm_loc * dtype_loc * sort_loc - | DTSort of sort_loc - | DTInd of Names.identifier Util.located * dtype_loc * Names.inductive * - sort_loc - | DTCoq of Term.types * dtype_loc * sort_loc -and dtype_loc = dtype Util.located - -val print_dtype_loc : - (Names.name * dtype_loc) list -> dtype_loc -> Pp.std_ppcmds -val print_dterm_loc : - (Names.name * dtype_loc) list -> dterm_loc -> Pp.std_ppcmds - -val sort_of_dtype_loc : - (Names.name * dtype_loc) list -> dtype_loc -> sort_loc - - -val infer : - (Names.name * dtype_loc) list -> Sast.term_loc -> dterm_loc * dtype_loc -val infer_type : (Names.name * dtype_loc) list -> Sast.type_loc -> dtype_loc diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml new file mode 100644 index 000000000..b6b763055 --- /dev/null +++ b/contrib/subtac/interp.ml @@ -0,0 +1,661 @@ +open Term +open Evarutil +open Evd +open Libnames +open Global +open Names +open Scoq +open Coqlib +open Pp +open Printer +open Subtac_errors +open Util +open Rawterm +open Context +open Eterm + +(* match t with + | RRef(loc, gr) -> + | RVar(loc, id) -> + | REvar(loc, e_key, arglopt) -> + | RPatVar(loc, (b * pvar)) -> + | RApp(loc, fn, args) -> + | RLambda(loc, name, typ, body) -> + | RProd(loc, name, dom, codom) -> + | RLetIn(loc, var, def, body) -> + | RLetTuple(loc, names, (name, expr), def, body) -> + | RIf(loc, cond, (name, expr), bodyl, bodyr) -> + | RRec(loc, fix_kind, identifiersarr, rawdecllistarray, + rawconstrarray, rawconstrarray) -> + | RSort(loc, rsort) -> + | RHole(loc, hole_kind) -> + | RCast(loc, expr, cast_kind, toexpr) -> + | RCases _ (* of loc * rawconstr option * + (rawconstr * (name * (loc * inductive * name list) option)) list * + (loc * identifier list * cases_pattern list * rawconstr) list *) -> + | RDynamic(loc, dynobj) -> + *) + + +type recursion_info = { + arg_name: identifier; + arg_type: types; (* A *) + wf_relation: constr; (* R : A -> A -> Prop *) + wf_proof: constr; (* : well_founded R *) + f_type: types; (* f: A -> Set *) + f_fulltype: types; (* Type with argument and wf proof product first *) +} + +type prog_info = { + evd : evar_defs ref; + mutable evm: evar_map; + rec_info: recursion_info option; +} + +let my_print_constr env ctx term = + Termops.print_constr_env (env_of_ctx env ctx) term + +let my_print_context env ctx = + Termops.print_rel_context (env_of_ctx env ctx) + +let my_print_rawconstr env ctx term = + Printer.pr_rawconstr_env (env_of_ctx env ctx) term + +let filter_defs l = List.filter (fun (_, c, _) -> c = None) l + +let evar_args ctx = + let rec aux acc i = function + (_, c, _) :: tl -> + (match c with + | None -> aux (mkRel i :: acc) (succ i) tl + | Some _ -> aux acc (succ i) tl) + | [] -> acc + in Array.of_list (aux [] 1 ctx) + +let evar_ctx prog_info ctx = + let ctx' = + match prog_info.rec_info with + Some ri -> + let len = List.length ctx in + assert(len >= 2); + let rec aux l acc = function + 0 -> + (match l with + (id, _, recf) :: arg :: [] -> arg :: (id, None, ri.f_fulltype) :: acc + | _ -> assert(false)) + | n -> (match l with + hd :: tl -> aux tl (hd :: acc) (pred n) + | _ -> assert(false)) + in + List.rev (aux ctx [] (len - 2)) + | None -> ctx + in filter_defs ctx' + + +let lookup_local env ctx (loc, id) = + try + let name = Name id in + let index, term, typ = Context.assoc_and_index name ctx in + let index = succ index in + let typ' = lift index typ in + debug 3 (str "Resolved " ++ str (string_of_id id) ++ str " locally as rel " ++ int index ++ str " : " ++ + my_print_constr env ctx typ' ++ str " in context: " ++ + my_print_context env ctx); + mkRel index, typ' + with Not_found -> + try + let (n,typ) = Termops.lookup_rel_id id (Environ.rel_context env) in + let index = List.length ctx + n in + mkRel index, (lift index) typ + with Not_found -> + try + let (_,_,typ) = Environ.lookup_named id env in + mkVar id, typ + with Not_found -> + Pretype_errors.error_var_not_found_loc loc id + +let pair_of_array a = (a.(0), a.(1)) +let make_name s = Name (id_of_string s) + +let app_opt c e = + match c with + Some constr -> constr e + | None -> e + +let rec disc_subset x = + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Ind i -> + let len = Array.length l in + let sig_ = Lazy.force sig_ in + if len = 2 && i = Term.destInd sig_.typ + then + let (a, b) = pair_of_array l in + Some (a, b) + else None + | _ -> None) + | _ -> None + +and disc_exist env ctx x = + trace (str "Disc_exist: " ++ my_print_constr env ctx x); + match kind_of_term x with + | App (c, l) -> + (match kind_of_term c with + Construct c -> + if c = Term.destConstruct (Lazy.force sig_).intro + then Some (l.(0), l.(1), l.(2), l.(3)) + else None + | _ -> None) + | _ -> None + + +let disc_proj_exist env ctx x = + trace (str "disc_proj_exist: " ++ my_print_constr env ctx x); + match kind_of_term x with + | App (c, l) -> + (if Term.eq_constr c (Lazy.force sig_).proj1 + && Array.length l = 3 + then disc_exist env ctx l.(2) + else None) + | _ -> None + + +let sort_rel s1 s2 = + match s1, s2 with + Prop Pos, Prop Pos -> Prop Pos + | Prop Pos, Prop Null -> Prop Null + | Prop Null, Prop Null -> Prop Null + | Prop Null, Prop Pos -> Prop Pos + | Type _, Prop Pos -> Prop Pos + | Type _, Prop Null -> Prop Null + | _, Type _ -> s2 + +let rec mu prog_info env ctx t = + match disc_subset t with + Some (u, p) -> + let f, ct = mu prog_info env ctx u in + (Some (fun x -> + app_opt f (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |]))), + ct) + | None -> (None, t) + +and coerce prog_info env ctx (x : Term.constr) (y : Term.constr) + : (Term.constr -> Term.constr) option + = + let rec coerce_unify ctx etyp argtyp = + match kind_of_term etyp, kind_of_term argtyp with + Evar (ev, args), _ -> + let evm = evars_of !(prog_info.evd) in + (*if is_defined evm ev then + coerce' ctx etyp (existential_value evm (ev, args)) + else ( *) + prog_info.evd := evar_define ev argtyp !(prog_info.evd); + debug 1 (str "Defining evar (evar to type) " ++ int ev ++ str " := " ++ my_print_constr env ctx argtyp); + None + | _, Evar (ev, args) -> + let evm = evars_of !(prog_info.evd) in + if is_defined evm ev then + coerce' ctx etyp (existential_value evm (ev, args)) + else ( + debug 1 (str "Defining evar (term to evar)" ++ int ev ++ str " := " ++ my_print_constr env ctx etyp); + prog_info.evd := evar_define ev etyp !(prog_info.evd); + None) + | _, _ -> coerce' ctx etyp argtyp + and coerce' ctx x y : (Term.constr -> Term.constr) option = + let subco () = subset_coerce ctx x y in + trace (str "Coercion from " ++ (my_print_constr env ctx x) ++ + str " to "++ my_print_constr env ctx y); + match (kind_of_term x, kind_of_term y) with + | Sort s, Sort s' -> + (match s, s' with + Prop x, Prop y when x = y -> None + | Prop _, Type _ -> None + | Type x, Type y when x = y -> None (* false *) + | _ -> subco ()) + | Prod (name, a, b), Prod (name', a', b') -> + let c1 = coerce_unify ctx a' a in + let c2 = coerce_unify ((name', None, a') :: ctx) b b' in + (match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun f -> + mkLambda (name', a', + app_opt c2 + (mkApp (Term.lift 1 f, + [| app_opt c1 (mkRel 1) |]))))) + + | App (c, l), App (c', l') -> + (match kind_of_term c, kind_of_term c' with + Ind i, Ind i' -> + let len = Array.length l in + let existS = Lazy.force existS in + if len = Array.length l' && len = 2 + && i = i' && i = Term.destInd existS.typ + then + begin (* Sigma types *) + debug 1 (str "In coerce sigma types"); + let (a, pb), (a', pb') = + pair_of_array l, pair_of_array l' + in + let c1 = coerce_unify ctx a a' in + let remove_head c = + let (_, _, x) = Term.destProd c in + x + in + let b, b' = remove_head pb, remove_head pb' in + let ctx' = (make_name "x", None, a) :: ctx in + let c2 = coerce_unify ctx' b b' in + match c1, c2 with + None, None -> None + | _, _ -> + Some + (fun x -> + let x, y = + app_opt c1 (mkApp (existS.proj1, + [| a; pb; x |])), + app_opt c2 (mkApp (existS.proj2, + [| a; pb'; x |])) + in + mkApp (existS.intro, [| x ; y |])) + end + else subco () + | _ -> subco ()) + | _, _ -> subco () + + and subset_coerce ctx x y = + match disc_subset x with + Some (u, p) -> + let c = coerce_unify ctx u y in + let f x = + app_opt c (mkApp ((Lazy.force sig_).proj1, + [| u; p; x |])) + in Some f + | None -> + match disc_subset y with + Some (u, p) -> + let c = coerce_unify ctx x u in + let evarinfo x = + let cx = app_opt c x in + let pcx = mkApp (p, [| cx |]) in + let ctx', pcx' = subst_ctx ctx pcx in + cx, { + Evd.evar_concl = pcx'; + Evd.evar_hyps = + Environ.val_of_named_context (evar_ctx prog_info ctx'); + Evd.evar_body = Evd.Evar_empty; + } + in + Some + (fun x -> + let key = mknewexist () in + let cx, evi = evarinfo x in + prog_info.evm <- Evd.add prog_info.evm key evi; + (mkApp + ((Lazy.force sig_).intro, + [| u; p; cx; + mkEvar (key, evar_args ctx) |]))) + | None -> + (try + let cstrs = Reduction.conv (Global.env ()) x y + in + ignore(Univ.merge_constraints cstrs (Global.universes ())); + Some (fun x -> + mkCast (x, DEFAULTcast, y)) + with + Reduction.NotConvertible -> + subtyping_error + (UncoercibleRewrite (my_print_constr env ctx x, + my_print_constr env ctx y)) + | e -> raise e) + + + in + try ignore(Reduction.conv_leq (Global.env ()) x y); None + with Reduction.NotConvertible -> coerce_unify ctx x y (* head recutions needed *) + + +and interp prog_info env ctx t : constr * constr (* The term -> its coq translation, its coq (not algorithmic) type *) = + let error s = anomaly ("subtac.interp: " ^ s) in + debug 1 (str "Interpreting term: " ++ my_print_rawconstr env ctx t ++ str " in env : " ++ + my_print_context env ctx); + + let rec type_app ctx (locf, coqf, ftyp) (e : rawconstr) = + let coercef, support = mu prog_info env ctx ftyp in + let narg, argtyp, restyp = + try + match decompose_prod_n 1 support with + [x, y], z -> x, y, z + | _ -> typing_error (NonFunctionalApp (locf, my_print_constr env ctx coqf, my_print_constr env ctx support, + my_print_rawconstr env ctx e)) + with _ -> typing_error (NonFunctionalApp (locf, my_print_constr env ctx coqf, my_print_constr env ctx support, + my_print_rawconstr env ctx e)) + in + let coqe, etyp = aux ctx e in + let _ = debug 2 (str "Coercion for application: " ++ + my_print_constr env ctx coqf ++ str " : " ++ + my_print_constr env ctx ftyp ++ str " and " ++ + my_print_constr env ctx coqe ++ str " : " ++ + my_print_constr env ctx etyp) + in + let coercee = coerce prog_info env ctx etyp argtyp in + let coqe' = app_opt coercee coqe in + let restype' = Term.subst1 coqe' restyp in + let call = + let len = List.length ctx in + let cf = app_opt coercef coqf in + match prog_info.rec_info with + Some r -> + (match kind_of_term cf with + Rel i when i = (pred len) -> + debug 3 (str "Spotted recursive call!"); + let ctx', proof = + subst_ctx ctx (mkApp (r.wf_relation, + [| coqe'; mkRel len |])) + in + let evarinfo = + { + Evd.evar_concl = proof; + Evd.evar_hyps = + Environ.val_of_named_context + (evar_ctx prog_info ctx'); + Evd.evar_body = Evd.Evar_empty; + } + in + let key = mknewexist () in + prog_info.evm <- Evd.add prog_info.evm key evarinfo; + mkApp (cf, [| coqe'; mkEvar(key, evar_args ctx) |]) + | _ -> mkApp (cf, [| coqe' |])) + | None -> mkApp (cf, [| coqe' |]) + in + debug 2 (str "Term obtained after coercion (at application): " ++ + Termops.print_constr_env (env_of_ctx env ctx) call); + call, restype' + + and aux ctx = function + | RRef(loc, gr) -> + (match gr with + | VarRef var -> + let coqt = type_of_global gr in + mkVar var, coqt + | ConstRef const -> + let coqt = type_of_global gr in + mkConst const, coqt + | IndRef ind -> + let coqt = type_of_global gr in + mkInd ind, coqt + | ConstructRef constr -> + let coqt = type_of_global gr in + mkConstruct constr, coqt) + + | RVar(loc, id) -> lookup_local env ctx (loc, id) + + | RApp(loc, fn, args) as x -> + let loc = loc_of_rawconstr fn in + debug 1 (str "Interpreting application: " ++ my_print_rawconstr env ctx x); + let coqfn, fntyp = aux ctx fn in +(* let coqfn, fntyp, args = + match kind_of_term coqfn with + Ind i -> + let len = List.length args in + debug 1 (my_print_constr env ctx coqfn ++ str " inductive applied to " ++ int len ++ str " arguments: " ++ + List.fold_left (fun acc arg -> acc ++ str " " ++ my_print_rawconstr env ctx arg) (str "") args + ); + let sig_ = Lazy.force sig_ in + if len = 2 && i = Term.destInd sig_.typ + then + let b = match args with [a;b] -> b | _ -> error "Partially applied subset type constructor" in + let coqb, btyp = aux ctx b in + (match kind_of_term coqb with + | Lambda (n, t, b) -> + mkApp (coqfn, [|t; coqb|]), mkSort (mk_Set), [] + | _ -> + debug 1 (my_print_constr env ctx btyp ++ str " is not a lambda") ; + error "Ill-typed subset type: ") + else if len = 3 && i = Term.destInd (Lazy.force eqind) + then + let b,c = match args with [a;b;c] -> b,c | _ -> error "Partially applied eq type constructor" in + let coqb, btyp = aux ctx b in + mkApp (coqfn, [|btyp; coqb|]), mkProd (Anonymous, btyp, mkSort (mk_Prop)), [c] + else ( + debug 1 (str "Not an eq or sig: " ++ my_print_constr env ctx coqfn); + coqfn, fntyp, args) + | x -> + debug 1 (str "Not an inductive: " ++ my_print_constr env ctx coqfn); + coqfn, fntyp, args + in*) + let _, term, typ = + List.fold_left (fun (loc, coqfn, fntyp) (e : rawconstr) -> + let coqfn', fntyp' = type_app ctx (loc, coqfn, fntyp) e in + join_loc loc (loc_of_rawconstr e), coqfn', fntyp') + (loc, coqfn, fntyp) args + in term, typ + + | RLambda(loc, name, argtyp, body) -> + let coqargtyp, argtyptyp = aux ctx argtyp in + let coqbody, bodytyp = aux ((name, None, coqargtyp) :: ctx) body in + let prod = mkProd (name, coqargtyp, bodytyp) in + (* Check it is well sorted *) + (*let coqprod, prodtyp = aux ctx prod in + if not (isSort prodtyp) then + typing_error (IllSorted (loc, my_print_constr env ctx prodtyp));*) + let coqlambda = mkLambda (name, coqargtyp, coqbody) in + (coqlambda, prod) + + | RProd(loc, name, dom, codom) -> + let coqdom, domtyp = aux ctx dom in + let coqcodom, codomtyp = aux ((name, None, coqdom) :: ctx) codom in + let s1, s2 = destSort domtyp, destSort codomtyp in + let s3 = sort_rel s1 s2 in + mkProd (name, coqdom, coqcodom), mkSort s3 + + | RLetIn(loc, var, def, body) -> + let coqdef, deftyp = aux ctx def in + let coqbody, bodytyp = aux ((var, Some coqdef, deftyp) :: ctx) body in + mkLetIn (var, coqdef, deftyp, coqbody), + Term.subst1 coqdef bodytyp + + | RLetTuple(loc, names, (name, expr), def, body) -> error "Let tuple : Not implemented" + + | RIf(loc, cond, (name, expr), bodyl, bodyr) -> + error "If: not implemented" + + | RRec(loc, fix_kind, identifiersarr, rawdecllistarray, + rawconstrarray, rawconstrarray2) -> + error "Rec : Not implemented" + + | RSort(loc, rsort) -> + let x, y = + (match rsort with + RProp Pos -> mk_Set, type_0 + | RProp Null -> mk_Prop, type_0 + | RType None -> type_0, type_0 + | RType (Some u) -> Type u, type_0) + in mkSort x, mkSort y + + | RHole(loc, k) -> + let ty = Evarutil.e_new_evar prog_info.evd env ~src:(loc,InternalHole) (Termops.new_Type ()) in + (Evarutil.e_new_evar prog_info.evd env ~src:(loc,k) ty), ty + + | RCast(loc, expr, cast_kind, toexpr) -> + let coqexpr, exprtyp = aux ctx expr in + let coqtoexpr, toexprtyp = aux ctx toexpr in + mkCast (coqexpr, cast_kind, coqtoexpr), toexprtyp + + + | RCases _ (* of loc * rawconstr option * + (rawconstr * (name * (loc * inductive * name list) option)) list * + (loc * identifier list * cases_pattern list * rawconstr) list *) -> + anomaly "Not implemented" + + | REvar(loc, e_key, arglopt) -> + let evm = evars_of !(prog_info.evd) in + let evi = map evm e_key in + let args = + match arglopt with + Some l -> Array.of_list (List.map (fun e -> fst (aux ctx e)) l) + | None -> [||] + in + (match evi.evar_body with + Evar_defined v -> mkApp (v, args), evi.evar_concl + | _ -> + mkEvar (e_key, args), evi.evar_concl) + + | RPatVar(loc, (b, pvar)) -> error "Found a pattern variable in a term to be typed" + | RDynamic(loc, d) -> + if (Dyn.tag d) = "constr" then + let c = Pretyping.constr_out d in + let j = (Retyping.get_type_of env Evd.empty c) in + j, c + else + user_err_loc (loc,"subtac.interp",(str "Not a constr tagged Dynamic")) + in aux ctx t + + +let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition +let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition + +let make_fixpoint t id term = + let term' = mkLambda (Name id, t.f_fulltype, term) in + mkApp (Lazy.force fix, + [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; + mkLambda (Name t.arg_name, t.arg_type, term') |]) + +let merge_evms x y = + Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y + +let subtac' recursive id env (s, t) = + check_required_library ["Coq";"Init";"Datatypes"]; + check_required_library ["Coq";"Init";"Specif"]; + try + let evm = Evd.empty in + let coqintern = Constrintern.intern_constr evm env in + let coqinterp = Constrintern.interp_constr evm env in + let s, t = coqintern s, coqintern t in + let prog_info = { evd = ref (Evd.create_evar_defs evm); evm = evm; rec_info = None } in + trace (str "Begin infer_type of given spec"); + let (evs, coqs) = Pretyping.understand_tcc evm env s and (evt, coqt) = Pretyping.understand_tcc evm env t in + debug 1 (str "Coq understands as : " ++ my_print_constr env [] coqs ++ str " : " ++ my_print_constr env [] coqt); + + + let coqtype, prog_info, ctx = + match recursive with + Some (n, t, rel, proof) -> + let coqrel = coqinterp rel in + let t', ttyp = interp prog_info env [] (coqintern t) in + let namen = Name n in + let coqs, styp = interp prog_info env [namen, None, t'] s in + let ftype = mkProd (namen, t', coqs) in + let fulltype = + mkProd (namen, t', + mkProd(Anonymous, + mkApp (coqrel, [| mkRel 1; mkRel 2 |]), + Term.subst1 (mkRel 2) coqs)) + in + let proof = + match proof with + ManualProof p -> (* TODO: Check that t is a proof of well_founded rel *) + coqinterp p + | AutoProof -> + (try Lazy.force (Hashtbl.find wf_relations coqrel) + with Not_found -> + msg_warning + (str "No proof found for relation " + ++ my_print_constr env [] coqrel); + raise Not_found) + | ExistentialProof -> + let wf_rel = mkApp (Lazy.force well_founded, [| t'; coqrel |]) in + let key = mknewexist () in + prog_info.evm <- Evd.add prog_info.evm key + { Evd.evar_concl = wf_rel; + Evd.evar_hyps = Environ.empty_named_context_val; + Evd.evar_body = Evd.Evar_empty }; + mkEvar (key, [| |]) + in + let prog_info = + let rec_info = + { arg_name = n; + arg_type = t'; + wf_relation = coqrel; + wf_proof = proof; + f_type = ftype; + f_fulltype = fulltype; + } + in { prog_info with rec_info = Some rec_info } + in + let coqctx = + [(Name id, None, ftype); (namen, None, t')] + in coqs, prog_info, coqctx + | None -> + let coqs, _ = interp prog_info env [] s in + coqs, prog_info, [] + in + trace (str "Rewrite of spec done:" ++ my_print_constr env ctx coqtype); + let coqt, ttyp = interp prog_info env ctx t in + trace (str "Interpretation done:" ++ spc () ++ + str "Interpreted term: " ++ my_print_constr env ctx coqt ++ spc () ++ + str "Infered type: " ++ my_print_constr env ctx ttyp); + + let coercespec = coerce prog_info env ctx ttyp coqtype in + trace (str "Specs coercion successfull"); + let realt = app_opt coercespec coqt in + trace (str "Term Specs coercion successfull" ++ + my_print_constr env ctx realt); + let realt = + match prog_info.rec_info with + Some t -> make_fixpoint t id realt + | None -> realt + in + let realt = Evarutil.whd_ise (evars_of !(prog_info.evd)) realt in + trace (str "Coq term" ++ my_print_constr env [] realt); + trace (str "Coq type" ++ my_print_constr env [] coqtype); + let evm = prog_info.evm in + (try trace (str "Original evar map: " ++ Evd.pr_evar_map evm); + with Not_found -> trace (str "Not found in pr_evar_map")); + let tac = Eterm.etermtac (evm, realt) in + msgnl (str "Starting proof"); + Command.start_proof id goal_kind coqtype (fun _ _ -> ()); + msgnl (str "Started proof"); + Pfedit.by tac + with + | Typing_error e -> + msg_warning (str "Type error in Program tactic:"); + let cmds = + (match e with + | NonFunctionalApp (loc, x, mux, e) -> + str "non functional application of term " ++ + e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux + | NonSigma (loc, t) -> + str "Term is not of Sigma type: " ++ t + | NonConvertible (loc, x, y) -> + str "Unconvertible terms:" ++ spc () ++ + x ++ spc () ++ str "and" ++ spc () ++ y + | IllSorted (loc, t) -> + str "Term is ill-sorted:" ++ spc () ++ t + ) + in msg_warning cmds + + | Subtyping_error e -> + msg_warning (str "(Program tactic) Subtyping error:"); + let cmds = + match e with + | UncoercibleInferType (loc, x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + | UncoercibleInferTerm (loc, x, y, tx, ty) -> + str "Uncoercible terms:" ++ spc () + ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x + ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y + | UncoercibleRewrite (x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + in msg_warning cmds + + | e -> + msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e)) + (*raise e*) + +let subtac recursive id env (s, t) = + subtac' recursive id (Global.env ()) (s, t) diff --git a/contrib/subtac/natural.ml b/contrib/subtac/natural.ml deleted file mode 100644 index a76d7357b..000000000 --- a/contrib/subtac/natural.ml +++ /dev/null @@ -1,10 +0,0 @@ -type nat = int - -let (+) (x : nat) (y : nat) = x + y -let (-) (x : nat) (y : nat) = - if y > x then raise (Invalid_argument "in substraction") - else x - y - -let succ (x : nat) = succ x - -let (<) (x : nat) (y : nat) = x < y diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml deleted file mode 100644 index afbbd18af..000000000 --- a/contrib/subtac/rewrite.ml +++ /dev/null @@ -1,682 +0,0 @@ -open Evd -open Libnames -open Coqlib -open Natural -open Infer -open Term -open Names -open Scoq -open Pp -open Printer -open Util - -type recursion_info = { - arg_name: identifier; - arg_type: types; (* A *) - wf_relation: constr; (* R : A -> A -> Prop *) - wf_proof: constr; (* : well_founded R *) - f_type: types; (* f: A -> Set *) - f_fulltype: types; (* Type with argument and wf proof product first *) -} - -let id_of_name = function - Name id -> id - | Anonymous -> raise (Invalid_argument "id_of_name") - -let rel_to_vars ctx constr = - let rec aux acc = function - (n, _, _) :: ctx -> - aux (Term.subst1 (mkVar n) acc) ctx - | [] -> acc - in aux constr ctx - -let subst_ctx ctx c = - let rec aux ((ctx, n, c) as acc) = function - (name, None, typ) :: tl -> - aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), - pred n, c) tl - | (name, Some term, typ) :: tl -> - let t' = Term.substnl [term] n c in - aux (ctx, n, t') tl - | [] -> acc - in - let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in - (x, rel_to_vars x z) - -(* Anotation needed for failed generalization *) -let named_context_of_ctx ctx : Sign.named_context = - List.fold_right - (fun (name, x, t) ctx -> - let x' = match x with - Some e -> Some (rel_to_vars ctx e) - | None -> None - and t' = rel_to_vars ctx t in - (id_of_name name, x', t') :: ctx) - ctx [] - -let env_of_ctx ctx : Environ.env = - Environ.push_rel_context ctx (Global.env ()) - -let rels_of_ctx ctx = - let n = List.length ctx in - Array.init n (fun i -> mkRel (n - i)) - -type prog_info = { - mutable evm: evar_map; - rec_info: recursion_info option; -} - -let my_print_constr ctx term = - Termops.print_constr_env (env_of_ctx ctx) term - -let my_print_context ctx = - Termops.print_rel_context (env_of_ctx ctx) - -let pair_of_array a = (a.(0), a.(1)) -let make_name s = Name (id_of_string s) - -let app_opt c e = - match c with - Some constr -> constr e - | None -> e - -(* Standard ? *) -let unlift n c = - let rec aux n acc = - if n = 0 then acc - else aux (pred n) (Termops.pop acc) - in aux n c - -let filter_defs l = List.filter (fun (_, c, _) -> c = None) l - -let evar_args ctx = - let n = List.length ctx in - let rec aux acc i = function - (_, c, _) :: tl -> - (match c with - | None -> aux (mkRel i :: acc) (succ i) tl - | Some _ -> aux acc (succ i) tl) - | [] -> acc - in Array.of_list (aux [] 1 ctx) - -let evar_ctx prog_info ctx = - let ctx' = - match prog_info.rec_info with - Some ri -> - let len = List.length ctx in - assert(len >= 2); - let rec aux l acc = function - 0 -> - (match l with - (id, _, recf) :: arg :: [] -> arg :: (id, None, ri.f_fulltype) :: acc - | _ -> assert(false)) - | n -> (match l with - hd :: tl -> aux tl (hd :: acc) (pred n) - | _ -> assert(false)) - in - List.rev (aux ctx [] (len - 2)) - | None -> ctx - in filter_defs ctx' - -let if_branches c = - match kind_of_term c with - | App (c, l) -> - (match kind_of_term c with - Ind i -> - let len = Array.length l in - if len = 2 - then - let (a, b) = pair_of_array l in - Some (i, (a,b)) - else None - | _ -> None) - | _ -> None - -let disc_proj_exist ctx x = - trace (str "disc_proj_exist: " ++ my_print_constr ctx x); - match kind_of_term x with - | App (c, l) -> - (if Term.eq_constr c (Lazy.force sig_).proj1 - && Array.length l = 3 - then - (match kind_of_term l.(2) with - App (c, l) -> - (match kind_of_term c with - Construct c -> - if c = Term.destConstruct (Lazy.force sig_).intro - && Array.length l = 4 - then - Some (l.(0), l.(1), l.(2), l.(3)) - else None - | _ -> None) - | _ -> None) - else None) - | _ -> None - -let rec rewrite_type prog_info ctx ((loc, t) as lt) : Term.types * Term.types = - trace (str "rewrite_type: " ++ print_dtype_loc [] lt); - trace (str "context: " ++ my_print_context ctx); - let aux prog_info ctx x = fst (rewrite_type prog_info ctx x) in - match t with - DTPi ((name, a), b, s) -> - let ta = aux prog_info ctx a in - let ctx' = (snd name, None, ta) :: ctx in - (mkProd (snd name, ta, aux prog_info ctx' b)), mkSort (snd s) - - | DTSigma ((name, a), b, s) -> - let ta = aux prog_info ctx a in - let ctx' = (snd name, None, ta) :: ctx in - mkApp ((Lazy.force existS).typ, - [| ta; - mkLambda - (snd name, ta, aux prog_info ctx' b) |]), - mkSort (snd s) - - | DTSubset ((name, a), b, s) -> - let ta = aux prog_info ctx a in - let name = Name (snd name) in - let ctx' = (name, None, ta) :: ctx in - (mkApp ((Lazy.force sig_).typ, - [| ta; mkLambda (name, ta, aux prog_info ctx' b) |])), - mkSort (snd s) - - | DTRel i -> - let (_, term, typ) = List.nth ctx i in - let t = - (*match term with - Some t -> Term.lift (succ i) t - | None -> *)mkRel (succ i) - in t, Term.lift (succ i) typ - - | DTApp (x, y, t, _) -> - let (cx, tx), (cy, ty) = - rewrite_type prog_info ctx x, rewrite_type prog_info ctx y - in - let coercex, coqx = mutype prog_info ctx tx in - let narg, targ, tres = - match decompose_prod_n 1 coqx with - [x, y], z -> x, y, z - | _ -> assert(false) - in - debug 2 (str "Coercion for type application: " ++ - my_print_constr ctx cx ++ spc () - ++ my_print_constr ctx cy); - let coercey = coerce prog_info ctx ty targ in - let t' = Term.subst1 (app_opt coercey cy) tres in - let term = mkApp (app_opt coercex cx, [|app_opt coercey cy|]) in - debug 1 (str "Term obtained after coercion (at application): " ++ - my_print_constr ctx term); - term, t' - - | DTCoq (t, dt, _) -> - (* type should be equivalent to 'aux prog_info ctx dt' *) - t, Typing.type_of (env_of_ctx ctx) prog_info.evm t - | DTTerm (t, dt, _) -> rewrite_term prog_info ctx t - | DTSort s -> mkSort (snd s), mkSort type_0 (* false *) - | DTInd (_, t, i, s) -> - let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in - mkInd i, ind.Declarations.mind_nf_arity - -and mutype prog_info ctx t = - match disc_subset t with - Some (u, p) -> - let f, ct = mutype prog_info ctx u in - (Some (fun x -> - app_opt f (mkApp ((Lazy.force sig_).proj1, - [| u; p; x |]))), - ct) - | None -> (None, t) - -and muterm prog_info ctx t = mutype prog_info ctx t - -and coerce' prog_info ctx x y : (Term.constr -> Term.constr) option = - let subco () = subset_coerce prog_info ctx x y in - trace (str "Coercion from " ++ (my_print_constr ctx x) ++ - str " to "++ my_print_constr ctx y); - match (kind_of_term x, kind_of_term y) with - | Sort s, Sort s' -> - (match s, s' with - Prop x, Prop y when x = y -> None - | Prop _, Type _ -> None - | Type x, Type y when x = y -> None (* false *) - | _ -> subco ()) - | Prod (name, a, b), Prod (name', a', b') -> - let c1 = coerce prog_info ctx a' a in - let bsubst = Term.subst1 (app_opt c1 (mkRel 1)) b in - let c2 = coerce prog_info ((name', None, a') :: ctx) bsubst b' in - (match c1, c2 with - None, None -> None - | _, _ -> - Some - (fun f -> - mkLambda (name', a', - app_opt c2 - (mkApp (Term.lift 1 f, - [| app_opt c1 (mkRel 1) |]))))) - - | App (c, l), App (c', l') -> - (match kind_of_term c, kind_of_term c' with - Ind i, Ind i' -> - let len = Array.length l in - let existS = Lazy.force existS and sig_ = Lazy.force sig_ in - if len = Array.length l' && len = 2 - && i = i' && i = Term.destInd existS.typ - then - begin (* Sigma types *) - debug 1 (str "In coerce sigma types"); - let (a, pb), (a', pb') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce prog_info ctx a a' in - let remove_head c = - let (_, _, x) = Term.destProd c in - x - in - let b, b' = remove_head pb, remove_head pb' in - let b'subst = - match c1 with - None -> b' - | Some c1 -> Term.subst1 (c1 (mkRel 1)) b' - in - let ctx' = (make_name "x", None, a) :: ctx in - let c2 = coerce prog_info ctx' b b'subst in - match c1, c2 with - None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt c1 (mkApp (existS.proj1, - [| a; pb; x |])), - app_opt c2 (mkApp (existS.proj2, - [| a; pb'; x |])) - in - mkApp (existS.intro, [| x ; y |])) - end - else subco () - | _ -> subco ()) - | _, _ -> subco () - -and coerce prog_info ctx (x : Term.constr) (y : Term.constr) - : (Term.constr -> Term.constr) option - = - try let cstrs = Reduction.conv_leq (Global.env ()) x y in None - with Reduction.NotConvertible -> coerce' prog_info ctx x y - -and disc_subset x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Ind i -> - let len = Array.length l in - let sig_ = Lazy.force sig_ in - if len = 2 && i = Term.destInd sig_.typ - then - let (a, b) = pair_of_array l in - Some (a, b) - else None - | _ -> None) - | _ -> None - -and disc_exist ctx x = - trace (str "Disc_exist: " ++ my_print_constr ctx x); - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Construct c -> - if c = Term.destConstruct (Lazy.force sig_).intro - then Some (l.(0), l.(1), l.(2), l.(3)) - else None - | _ -> None) - | _ -> None - -and subset_coerce prog_info ctx x y = - match disc_subset x with - Some (u, p) -> - let c = coerce prog_info ctx u y in - let f x = - app_opt c (mkApp ((Lazy.force sig_).proj1, - [| u; p; x |])) - in Some f - | None -> - match disc_subset y with - Some (u, p) -> - let c = coerce prog_info ctx x u in - let t = id_of_string "t" in - let evarinfo x = - let cx = app_opt c x in - let pcx = mkApp (p, [| cx |]) in - let ctx', pcx' = subst_ctx ctx pcx in - cx, { - Evd.evar_concl = pcx'; - Evd.evar_hyps = - Environ.val_of_named_context (evar_ctx prog_info ctx'); - Evd.evar_body = Evd.Evar_empty; - } - in - Some - (fun x -> - let key = mknewexist () in - let cx, evi = evarinfo x in - prog_info.evm <- Evd.add prog_info.evm key evi; - (mkApp - ((Lazy.force sig_).intro, - [| u; p; cx; - mkEvar (key, evar_args ctx) |]))) - | None -> - (try - let cstrs = Reduction.conv (Global.env ()) x y - in - ignore(Univ.merge_constraints cstrs (Global.universes ())); - Some (fun x -> - mkCast (x, DEFAULTcast, y)) - with - Reduction.NotConvertible -> - subtyping_error - (UncoercibleRewrite (my_print_constr ctx x, - my_print_constr ctx y)) - | e -> raise e) - -and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types = - let rec aux ctx (loc, t) = - match t with - | DRel i -> - let (_, term, typ) = List.nth ctx i in - let t = mkRel (succ i) in - t, Term.lift (succ i) typ - - | DLambda ((name, targ), e, t) -> - let argt, argtt = rewrite_type prog_info ctx targ in - let coqe, et = - rewrite_term prog_info ((snd name, None, argt) :: ctx) e - in - let coqt = mkLambda (snd name, argt, coqe) - and t = mkProd (snd name, argt, et) in - (coqt, t) - - | DApp (f, e, t) -> - let cf, ft = rewrite_term prog_info ctx f in - let coercef, coqt = muterm prog_info ctx ft in - let narg, targ, tres = - match decompose_prod_n 1 coqt with - [x, y], z -> x, y, z - | _ -> assert(false) - in - let ce, te = rewrite_term prog_info ctx e in - debug 2 (str "Coercion for application" ++ - my_print_constr ctx cf ++ spc () - ++ my_print_constr ctx ce); - let call x = - let len = List.length ctx in - let cf = app_opt coercef cf in - match prog_info.rec_info with - Some r -> - (match kind_of_term cf with - Rel i when i = (pred len) -> - debug 3 (str "Spotted recursive call!"); - let ctx', proof = - subst_ctx ctx (mkApp (r.wf_relation, - [| x; mkRel len |])) - in - let evarinfo = - { - Evd.evar_concl = proof; - Evd.evar_hyps = - Environ.val_of_named_context - (evar_ctx prog_info ctx'); - Evd.evar_body = Evd.Evar_empty; - } - in - let key = mknewexist () in - prog_info.evm <- Evd.add prog_info.evm key evarinfo; - mkApp (cf, [| x; mkEvar(key, evar_args ctx) |]) - | _ -> mkApp (cf, [| x |])) - | None -> mkApp (cf, [| x |]) - in - let coercee = coerce prog_info ctx te targ in - let t' = Term.subst1 (app_opt coercee ce) tres in - let t = call (app_opt coercee ce) in - debug 2 (str "Term obtained after coercion (at application): " ++ - Termops.print_constr_env (env_of_ctx ctx) t); - t, t' - - | DSum ((x, t), (t', u), stype) -> - let ct, ctt = rewrite_term prog_info ctx t in - let ctxterm = (snd x, Some ct, ctt) :: ctx in - let ctxtype = (snd x, Some ct, ctt) :: ctx in - let ct', tt' = rewrite_term prog_info ctxterm t' in - let cu, _ = rewrite_type prog_info ctxtype u in - let coercet' = coerce prog_info ctxtype tt' cu in - let lam = Term.subst1 ct (app_opt coercet' ct') in - debug 1 (str "Term obtained after coercion: " ++ - Termops.print_constr_env (env_of_ctx ctx) lam); - - let t' = - mkApp ((Lazy.force existS).typ, - [| ctt; mkLambda (snd x, ctt, cu) |]) - in - mkApp ((Lazy.force existS).intro, - [| ctt ; mkLambda (snd x, ctt, cu); - ct; lam |]), t' - - | DLetIn (x, e, e', t) -> - let ce, et' = rewrite_term prog_info ctx e in - let ce', t' = aux ((snd x, (Some ce), et') :: ctx) e' in - mkLetIn (snd x, ce, et', ce'), t' - - | DLetTuple (l, e, e', t) -> - (* let (a, b) = e in e', l = [b, a] *) - let ce, et = rewrite_term prog_info ctx e in - debug 1 (str "Let tuple, e = " ++ - my_print_constr ctx ce ++ - str "type of e: " ++ my_print_constr ctx et); - let l, ctx' = - let rec aux acc ctx = function - (x, t, t') :: tl -> - let tx, _ = rewrite_type prog_info ctx t in - let trest, _ = rewrite_type prog_info ctx t' in - let ctx' = (snd x, None, tx) :: ctx in - aux ((x, tx, trest) :: acc) ctx' tl - | [] -> (acc), ctx - in aux [] ctx (List.rev l) - in - let ce', et' = aux ctx' e' in - let et' = mkLambda (Anonymous, et, - unlift (pred (List.length l)) et') in - debug 1 (str "Let tuple, type of e': " ++ - my_print_constr ctx' et'); - - let ind = destInd (Lazy.force existSind) in - let ci = Inductiveops.make_default_case_info - (Global.env ()) RegularStyle ind - in - let lambda = - let rec aux acc = function - (x, t, tt) :: (_ :: _) as tl -> - let lam = mkLambda (snd x, t, acc) in - let term = - mkLambda (make_name "dummy", tt, - mkCase (ci, et', mkRel 1, [| lam |])) - in aux term tl - | (x, t, _) :: [] -> - let lam = mkLambda (snd x, t, acc) in - mkCase (ci, et', ce, [| lam |]) - | _ -> assert(false) - in - match l with - (x, t, t') :: tl -> - aux (mkLambda (snd x, t, ce')) tl - | [] -> failwith "DLetTuple with empty list!" - in - debug 1 (str "Let tuple term: " ++ my_print_constr ctx lambda); - lambda, et' - - | DIfThenElse (b, e, e', tif) -> - let name = Name (id_of_string "H") in - let (cb, tb) = aux ctx b in - (match if_branches tb with - Some (ind, (t, f)) -> - let ci = Inductiveops.make_default_case_info - (Global.env ()) IfStyle ind - in - let (ce, te), (ce', te') = - aux ((name, None, t) :: ctx) e, - aux ((name, None, f) :: ctx) e' - in - let lam = mkLambda (Anonymous, tb, te) in - let true_case = - mkLambda (name, t, ce) - and false_case = - mkLambda (name, f, ce') - in - (mkCase (ci, lam, cb, [| true_case; false_case |])), - (Termops.pop te) - | None -> failwith ("Ill-typed if")) - - - | DCoq (constr, t) -> constr, - Typing.type_of (env_of_ctx ctx) prog_info.evm constr - - in aux ctx t - -let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition -let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition - -let make_fixpoint t id term = - let term' = mkLambda (Name id, t.f_fulltype, term) in - mkApp (Lazy.force fix, - [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; - mkLambda (Name t.arg_name, t.arg_type, term') |]) - -let subtac recursive id (s, t) = - check_required_library ["Coq";"Init";"Datatypes"]; - check_required_library ["Coq";"Init";"Specif"]; - try - let prog_info = { evm = Evd.empty; rec_info = None } in - trace (str "Begin infer_type of given spec"); - let coqtype, coqtype', coqtype'', prog_info, ctx, coqctx = - match recursive with - Some (n, t, rel, proof) -> - let t' = infer_type [] t in - let namen = Name n in - let coqt = infer_type [namen, t'] s in - let t'', _ = rewrite_type prog_info [] t' in - let coqt', _ = rewrite_type prog_info [namen, None, t''] coqt in - let ftype = mkLambda (namen, t'', coqt') in - let fulltype = - mkProd (namen, t'', - mkProd(Anonymous, - mkApp (rel, [| mkRel 1; mkRel 2 |]), - Term.subst1 (mkRel 2) coqt')) - in - let proof = - match proof with - ManualProof p -> p (* Check that t is a proof of well_founded rel *) - | AutoProof -> - (try Lazy.force (Hashtbl.find wf_relations rel) - with Not_found -> - msg_warning - (str "No proof found for relation " - ++ my_print_constr [] rel); - raise Not_found) - | ExistentialProof -> - let wf_rel = mkApp (Lazy.force well_founded, [| t''; rel |]) in - let key = mknewexist () in - prog_info.evm <- Evd.add prog_info.evm key - { Evd.evar_concl = wf_rel; - Evd.evar_hyps = Environ.empty_named_context_val; - Evd.evar_body = Evd.Evar_empty }; - mkEvar (key, [| |]) - in - let prog_info = - let rec_info = - { arg_name = n; - arg_type = t''; - wf_relation = rel; - wf_proof = proof; - f_type = ftype; - f_fulltype = fulltype; - } - in { prog_info with rec_info = Some rec_info } - in - let coqtype = dummy_loc, - DTPi (((dummy_loc, namen), t'), coqt, - sort_of_dtype_loc [] coqt) - in - let coqtype' = mkProd (namen, t'', coqt') in - let ctx = [(Name id, coqtype); (namen, t')] - and coqctx = - [(Name id, None, coqtype'); (namen, None, t'')] - in coqt, coqt', coqtype', prog_info, ctx, coqctx - | None -> - let coqt = infer_type [] s in - let coqt', _ = rewrite_type prog_info [] coqt in - coqt, coqt', coqt', prog_info, [], [] - in - trace (str "Rewrite of coqtype done" ++ - str "coqtype' = " ++ pr_constr coqtype'); - let dterm, dtype = infer ctx t in - trace (str "Inference done" ++ spc () ++ - str "Infered term: " ++ print_dterm_loc ctx dterm ++ spc () ++ - str "Infered type: " ++ print_dtype_loc ctx dtype); - let dterm', dtype' = - fst (rewrite_term prog_info coqctx dterm), - fst (rewrite_type prog_info coqctx dtype) - in - trace (str "Rewrite done" ++ spc () ++ - str "Inferred Coq term:" ++ pr_constr dterm' ++ spc () ++ - str "Inferred Coq type:" ++ pr_constr dtype' ++ spc () ++ - str "Rewritten Coq type:" ++ pr_constr coqtype'); - let coercespec = coerce prog_info coqctx dtype' coqtype' in - trace (str "Specs coercion successfull"); - let realt = app_opt coercespec dterm' in - trace (str "Term Specs coercion successfull" ++ - my_print_constr coqctx realt); - let realt = - match prog_info.rec_info with - Some t -> make_fixpoint t id realt - | None -> realt - in - trace (str "Coq term" ++ my_print_constr [] realt); - trace (str "Coq type" ++ my_print_constr [] coqtype''); - let evm = prog_info.evm in - (try trace (str "Original evar map: " ++ Evd.pr_evar_map evm); - with Not_found -> trace (str "Not found in pr_evar_map")); - let tac = Eterm.etermtac (evm, realt) in - msgnl (str "Starting proof"); - Command.start_proof id goal_kind coqtype'' (fun _ _ -> ()); - msgnl (str "Started proof"); - Pfedit.by tac - with - | Typing_error e -> - msg_warning (str "Type error in Program tactic:"); - let cmds = - (match e with - | NonFunctionalApp (loc, x, mux) -> - str "non functional type app of term " ++ - x ++ str " of (mu) type " ++ mux - | NonSigma (loc, t) -> - str "Term is not of Sigma type: " ++ t - | NonConvertible (loc, x, y) -> - str "Unconvertible terms:" ++ spc () ++ - x ++ spc () ++ str "and" ++ spc () ++ y - ) - in msg_warning cmds - - | Subtyping_error e -> - msg_warning (str "(Program tactic) Subtyping error:"); - let cmds = - match e with - | UncoercibleInferType (loc, x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - | UncoercibleInferTerm (loc, x, y, tx, ty) -> - str "Uncoercible terms:" ++ spc () - ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x - ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y - | UncoercibleRewrite (x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - in msg_warning cmds - - | e -> raise e diff --git a/contrib/subtac/rewrite.mli b/contrib/subtac/rewrite.mli deleted file mode 100644 index 17660e14a..000000000 --- a/contrib/subtac/rewrite.mli +++ /dev/null @@ -1,3 +0,0 @@ -val subtac : - (Names.identifier * Sast.type_loc * Term.constr * Scoq.wf_proof_type) option -> - Names.identifier -> Sast.type_loc * Sast.term_loc -> unit diff --git a/contrib/subtac/sast.ml b/contrib/subtac/sast.ml deleted file mode 100644 index 4d0ca759d..000000000 --- a/contrib/subtac/sast.ml +++ /dev/null @@ -1,25 +0,0 @@ -open Names -open Util - -type const = CNat of int | CInt of int | CBool of bool - -type term = - SIdent of identifier located - | SLambda of (identifier located * type_ located) * term located - | SApp of term located * term located - | SLetIn of (name located) * (term located) * term located - | SLetTuple of (name located) list * term located * term located - | SIfThenElse of (term located) * (term located) * (term located) - | SSumInf of (term located) * (term located) - | SSumDep of (identifier located * term located) * (term located * type_ located) -and lettuple_el = (identifier located) option * term_loc * type_loc option -and term_loc = term located -and type_ = - | TApp of type_loc * type_loc - | TPi of (name located * type_loc) * type_loc - | TSigma of (name located * type_loc) * type_loc - | TSubset of (identifier located * type_loc) * type_loc - | TIdent of identifier located - | TTerm of term_loc - -and type_loc = type_ located diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml index 52acb845d..a864b95c9 100644 --- a/contrib/subtac/scoq.ml +++ b/contrib/subtac/scoq.ml @@ -1,7 +1,6 @@ open Evd open Libnames open Coqlib -open Natural open Term open Names @@ -16,6 +15,8 @@ let build_sig () = let sig_ = lazy (build_sig ()) +let eqind = lazy (gen_constant "subtac" ["Init"; "Logic"] "eq") + let boolind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "bool") let sumboolind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sumbool") let natind = lazy (gen_constant "subtac" ["Init"; "Datatypes"] "nat") @@ -66,7 +67,5 @@ let std_relations = Lazy.lazy_from_fun std_relations type wf_proof_type = AutoProof - | ManualProof of Term.constr + | ManualProof of Topconstr.constr_expr | ExistentialProof - -let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4 index dbb149c20..38ef0a7aa 100644 --- a/contrib/subtac/sparser.ml4 +++ b/contrib/subtac/sparser.ml4 @@ -24,8 +24,6 @@ open Term open Libnames open Topconstr -open Sast - (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac.<foo> *) @@ -38,8 +36,6 @@ module Subtac = struct let gec s = Gram.Entry.create ("Subtac."^s) (* types *) - let subtac_spec : type_loc Gram.Entry.e = gec "subtac_spec" - let subtac_term : term_loc Gram.Entry.e = gec "subtac_term" let subtac_wf_proof_type : Scoq.wf_proof_type Gram.Entry.e = gec "subtac_wf_proof_type" (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) @@ -85,144 +81,11 @@ open Subtac open Util GEXTEND Gram - GLOBAL: subtac_spec subtac_term subtac_wf_proof_type; - - (* Types ******************************************************************) - subtac_spec: - [ - "10" LEFTA - [ t = subtac_spec; t' = subtac_spec -> loc, TApp (t, t') ] - - | [ t = subtac_spec_no_app -> t ] - ]; - - subtac_spec_no_app: - [ [ - "(" ; t = subtac_spec_lpar_open -> t - | "[" ; x = subtac_binder_opt; "]"; t = subtac_spec -> - loc, TSigma (x, t) - | "{" ; x = subtac_binder; "|"; p = subtac_spec; "}"; "->"; t = subtac_spec -> - let ((locx, i), tx) = x in - loc, TPi (((locx, Name i), (loc, TSubset (x, p))), t) - | "{" ; x = subtac_binder; "|"; p = subtac_spec; "}" -> - loc, TSubset(x, p) - | t = subtac_type_ident; f = subtac_spec_tident -> f t - ] - ] - ; - - subtac_spec_no_app_loc: - [ [ x = subtac_spec_no_app -> (loc, x) ] - ]; - - subtac_spec_tident: - [ [ - "->"; t' = subtac_spec -> - fun t -> loc, TPi (((dummy_loc, Anonymous), t), t') - | -> (fun x -> x) - ] - ] - ; - - subtac_spec_lpar_open: - [ - [ s = subtac_identifier; t = subtac_spec_lpar_name -> t s - | s = subtac_spec; ")" -> s ] - ] - ; - - subtac_spec_lpar_name: - [ - [ ":" ; y = subtac_spec; ")"; t = subtac_spec -> - (fun s -> loc, TPi ((((fst s), Name (snd s)), y), t)) - | l = LIST1 subtac_spec_no_app_loc; ")" -> fun s -> - List.fold_left (fun acc x -> - (join_loc (fst acc) (fst x), TApp (acc, snd x))) - (fst s, TIdent s) l - ] - ] - ; - - subtac_binder: - [ [ s = subtac_identifier; ":"; t = subtac_spec -> let (l,s) = s in - ((loc, s), t) - | "{"; x = subtac_binder; "|"; p = subtac_spec; "}" -> - let ((l, s), t) = x in - ((l, s), (loc, TSubset (x, p))) - ] - ] - ; - - subtac_identifier: - [ [ s = IDENT -> (loc, id_of_string s) ] ] - ; - - subtac_real_name: - [ [ s = IDENT -> (loc, Name (id_of_string s)) - (* | "_" -> loc, Anonymous111 *) - ] ] - ; - - subtac_name: - [ [ n = OPT subtac_real_name -> match n with Some n -> n | None -> loc, Anonymous ] ] - ; - - subtac_binder_opt: - [ [ s = subtac_name; ":"; t = subtac_spec -> (s, t) ] ] - ; - - subtac_type_ident: - [ [ s = subtac_identifier -> loc, TIdent s ] ] - ; - - subtac_term: - [ - "20" LEFTA - [ t = subtac_term; t' = subtac_term -> - let loc = join_loc (fst t) (fst t') in - loc, SApp (t, t') - ] - | "10" - [ - i = subtac_identifier -> loc, SIdent i - | "fun"; bl = LIST1 subtac_binder; "=>"; p = subtac_term -> - (List.fold_left - (fun acc (((loc, s), (loc', t)) as b) -> - (join_loc loc (fst acc), SLambda (b, acc))) p bl) - | "let"; "("; nl = LIST0 subtac_name SEP ","; ")" ; "="; t = subtac_term; - "in"; t' = subtac_term -> - loc, (SLetTuple (nl, t, t')) - | "let"; i = subtac_name; "="; t = subtac_term; "in"; t' = subtac_term -> - loc, (SLetIn (i, t, t')) - | "if"; b = subtac_term; "then"; t = subtac_term; "else"; t' = subtac_term -> - loc, SIfThenElse (b, t, t') - | "("; t = subtac_lpar_term -> t - ] - - ] - ; - - subtac_lpar_term: - [ [ - x = test_id_coloneq; t = subtac_term; ","; - t' = subtac_term; ":"; tt = subtac_spec; ")" -> - (loc, (SSumDep (((dummy_loc, x), t), (t', tt)))) - | t = subtac_term; f = subtac_lpar_term_term -> f t - ] - ] - ; - - subtac_lpar_term_term: - [ [ - ","; t' = subtac_term; ")" -> - (fun t -> loc, (SSumInf (t, t'))) - | ")" -> (fun x -> x) - ] ] - ; - + GLOBAL: subtac_wf_proof_type; + subtac_wf_proof_type: [ [ IDENT "proof"; t = Constr.constr -> - Scoq.ManualProof (Scoq.constr_of t) + Scoq.ManualProof t | IDENT "auto" -> Scoq.AutoProof | -> Scoq.ExistentialProof ] @@ -230,20 +93,8 @@ GEXTEND Gram ; END -type type_loc_argtype = (type_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type -type term_loc_argtype = (term_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type type wf_proof_type_argtype = (Scoq.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type -let (wit_subtac_spec : type_loc_argtype), - (globwit_subtac_spec : type_loc_argtype), - (rawwit_subtac_spec : type_loc_argtype) = - Genarg.create_arg "subtac_spec" - -let (wit_subtac_term : term_loc_argtype), - (globwit_subtac_term : term_loc_argtype), - (rawwit_subtac_term : term_loc_argtype) = - Genarg.create_arg "subtac_term" - let (wit_subtac_wf_proof_type : wf_proof_type_argtype), (globwit_subtac_wf_proof_type : wf_proof_type_argtype), (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) = @@ -251,15 +102,14 @@ let (wit_subtac_wf_proof_type : wf_proof_type_argtype), VERNAC COMMAND EXTEND SubtacRec [ "Recursive" "program" ident(id) - "(" ident(recid) ":" subtac_spec(rect) ")" + "(" ident(recid) ":" constr(rect) ")" "using" constr(wf_relation) - subtac_wf_proof_type(wf) - ":" subtac_spec(s) ":=" subtac_term(t) ] -> - [ Rewrite.subtac (Some (recid, rect, - Scoq.constr_of wf_relation, wf)) id (s, t) ] + subtac_wf_proof_type(wf) + ":" constr(s) ":=" constr(t) ] -> + [ Interp.subtac (Some (recid, rect, wf_relation, wf)) id Environ.empty_env (s, t) ] END VERNAC COMMAND EXTEND Subtac -[ "Program" ident(id) ":" subtac_spec(s) ":=" subtac_term(t) ] -> -[ Rewrite.subtac None id (s, t) ] +[ "Program" ident(id) ":" operconstr(s) ":=" constr(t) ] -> + [ Interp.subtac None id Environ.empty_env (s, t) ] END diff --git a/contrib/subtac/sutils.ml b/contrib/subtac/sutils.ml deleted file mode 100644 index 64365b676..000000000 --- a/contrib/subtac/sutils.ml +++ /dev/null @@ -1,11 +0,0 @@ -let list_index x l = - let rec aux i = function - y :: tl -> if x = y then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -let list_assoc_index x l = - let rec aux i = function - (y, _) :: tl -> if x = y then i else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l diff --git a/contrib/subtac/sutils.mli b/contrib/subtac/sutils.mli deleted file mode 100644 index 00dd00b1c..000000000 --- a/contrib/subtac/sutils.mli +++ /dev/null @@ -1,3 +0,0 @@ -val list_index : 'a -> 'a list -> int -val list_assoc_index : 'a -> ('a * 'b) list -> int - |