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)