|
| 1 | +(** Goal. *) |
| 2 | + |
| 3 | +open Lplib open Base open Extra |
| 4 | +open Timed |
| 5 | +open Core open Term open Print |
| 6 | + |
| 7 | +type goal_typ = |
| 8 | + { goal_meta : meta (** Goal metavariable. *) |
| 9 | + ; goal_hyps : Env.t (** Precomputed scoping environment. *) |
| 10 | + ; goal_type : term (** Precomputed type. *) } |
| 11 | + |
| 12 | +type ('a,'b) t = Typ of 'a | Unif of 'b |
| 13 | + |
| 14 | +type goal = (goal_typ, constr) t |
| 15 | + |
| 16 | +let is_typ : goal -> bool = function Typ _ -> true | Unif _ -> false |
| 17 | +let is_unif : goal -> bool = function Typ _ -> false | Unif _ -> true |
| 18 | + |
| 19 | +let get_constr : goal -> constr = |
| 20 | + function Unif c -> c | Typ _ -> invalid_arg (__FILE__ ^ "get_constr") |
| 21 | + |
| 22 | +let get_names : goal -> int StrMap.t = function |
| 23 | + | Unif(c,_,_) -> Ctxt.names c |
| 24 | + | Typ gt -> Env.names gt.goal_hyps |
| 25 | + |
| 26 | +(** The string representation of a goal [g] is a tuple [(l,b,s,t)] where [l] |
| 27 | + is a list of pairs of strings [(assumption_name,assumption_type)] and, if |
| 28 | + [g] is a typing goal, then [b=true], [s] is the goal meta name and [t] is |
| 29 | + the goal type, and if [g] is a unification goal, then [b=false] and [s] |
| 30 | + and [t] are the LHS and RHS of the goal respectively. *) |
| 31 | +type info = (string * string) list * (string * string, string) t |
| 32 | + |
| 33 | +(** [ctxt g] returns the typing context of the goal [g]. *) |
| 34 | +let ctxt : goal -> ctxt = fun g -> |
| 35 | + match g with |
| 36 | + | Typ gt -> Env.to_ctxt gt.goal_hyps |
| 37 | + | Unif (c,_,_) -> c |
| 38 | + |
| 39 | +(** [env g] returns the scoping environment of the goal [g]. *) |
| 40 | +let env : goal -> Env.t = fun g -> |
| 41 | + match g with |
| 42 | + | Unif (c,_,_) -> |
| 43 | + let t, n = Ctxt.to_prod c mk_Type in |
| 44 | + (try fst (Env.of_prod_nth c n t) |
| 45 | + with Invalid_argument _ -> assert false) |
| 46 | + | Typ gt -> gt.goal_hyps |
| 47 | + |
| 48 | +(** [of_meta m] creates a goal from the meta [m]. *) |
| 49 | +let of_meta : meta -> goal = fun m -> |
| 50 | + let goal_hyps, goal_type = |
| 51 | + try Env.of_prod_nth [] m.meta_arity !(m.meta_type) |
| 52 | + with Invalid_argument _ -> assert false |
| 53 | + in |
| 54 | + Typ {goal_meta = m; goal_hyps; goal_type } |
| 55 | + |
| 56 | +(** [simpl_opt f g] tries to simplify the goal [g] with the function [f]. *) |
| 57 | +let simpl_opt : (ctxt -> term -> term option) -> goal -> goal option = |
| 58 | + fun f g -> |
| 59 | + match g with |
| 60 | + | Typ gt -> |
| 61 | + begin |
| 62 | + match f (Env.to_ctxt gt.goal_hyps) gt.goal_type with |
| 63 | + | None -> None |
| 64 | + | Some goal_type -> Some(Typ {gt with goal_type}) |
| 65 | + end |
| 66 | + | Unif(c,t,u) -> |
| 67 | + match f c t, f c u with |
| 68 | + | Some t, Some u -> Some(Unif(c,t,u)) |
| 69 | + | _ -> None |
| 70 | + |
| 71 | +(** [simpl f g] simplifies the goal [g] with the function [f]. *) |
| 72 | +let simpl : (ctxt -> term -> term) -> goal -> goal = fun f g -> |
| 73 | + match g with |
| 74 | + | Typ gt -> |
| 75 | + Typ {gt with goal_type = f (Env.to_ctxt gt.goal_hyps) gt.goal_type} |
| 76 | + | Unif (c,t,u) -> Unif (c, f c t, f c u) |
| 77 | + |
| 78 | +(** [typ_or_def idmap ppf (_,ty,def)] prints in [ppf] the type [ty] or the |
| 79 | + definition [def] if there is one. *) |
| 80 | +let typ_or_def idmap ppf (ty,def) = |
| 81 | + let term = term_in idmap in |
| 82 | + match def with |
| 83 | + | None -> out ppf "%a" term (Eval.snf_beta ty) |
| 84 | + | Some u -> out ppf "≔ %a" term u |
| 85 | + |
| 86 | +(** [ctxt_elt idmap ppf x] prints in [ppf] the conttext element [x]. *) |
| 87 | +let ctxt_elt idmap ppf (v,ty,def) = |
| 88 | + out ppf "%a%a" var v (typ_or_def idmap) (ty,def) |
| 89 | + |
| 90 | +(** [env_elt idmap ppf x] prints in [ppf] the environment element [x]. *) |
| 91 | +let env_elt idmap ppf (s,(_,ty,def)) = |
| 92 | + out ppf "%a%a" uid s (typ_or_def idmap) (ty,def) |
| 93 | + |
| 94 | +(** [hyps ppf g] prints on [ppf] the beta-normal forms of the hypotheses of |
| 95 | + the goal [g]. *) |
| 96 | +let hyps : int StrMap.t -> goal pp = |
| 97 | + let hyps elt ppf l = |
| 98 | + if l <> [] then |
| 99 | + out ppf "%a---------------------------------------------\ |
| 100 | + ---------------------------------\n" |
| 101 | + (List.pp (fun ppf -> out ppf "%a\n" elt) "") (List.rev l) |
| 102 | + in |
| 103 | + fun idmap ppf g -> |
| 104 | + match g with |
| 105 | + | Typ gt -> hyps (env_elt idmap) ppf gt.goal_hyps |
| 106 | + | Unif (c,_,_) -> hyps (ctxt_elt idmap) ppf c |
| 107 | + |
| 108 | +(** [concl ppf g] prints on [ppf] the beta-normal form of the conclusion of |
| 109 | + the goal [g]. *) |
| 110 | +let concl : int StrMap.t -> goal pp = fun idmap ppf g -> |
| 111 | + let term = term_in idmap in |
| 112 | + match g with |
| 113 | + | Typ gt -> |
| 114 | + out ppf "?%d: %a" gt.goal_meta.meta_key |
| 115 | + term (Eval.snf_beta gt.goal_type) |
| 116 | + | Unif (_, t, u) -> |
| 117 | + out ppf "%a ≡ %a" term (Eval.snf_beta t) term (Eval.snf_beta u) |
| 118 | + |
| 119 | +(** [pp ppf g] prints on [ppf] the beta-normal form of the goal [g] with its |
| 120 | + hypotheses. *) |
| 121 | +let pp ppf g = let idmap = get_names g in hyps idmap ppf g; concl idmap ppf g |
| 122 | + |
| 123 | +(** [pp_no_hyp ppf g] prints on [ppf] the beta-normal form of the conclusion |
| 124 | + of the goal [g] without its hypotheses. *) |
| 125 | +let pp_no_hyp ppf g = concl (get_names g) ppf g |
| 126 | + |
| 127 | +(** [to_info g] converts the goal [g] into an [info] data structure.*) |
| 128 | +let to_info : goal -> info = |
| 129 | + let buf = Buffer.create 80 in |
| 130 | + let ppf = Format.formatter_of_buffer buf in |
| 131 | + let to_string f x = |
| 132 | + f ppf x; |
| 133 | + Format.pp_print_flush ppf (); |
| 134 | + let res = Buffer.contents buf in |
| 135 | + Buffer.clear buf; |
| 136 | + res |
| 137 | + in |
| 138 | + fun g -> |
| 139 | + let idmap = get_names g in |
| 140 | + let term = term_in idmap in |
| 141 | + match g with |
| 142 | + | Typ gt -> |
| 143 | + let f (s,(_,ty,def)) = s, to_string (typ_or_def idmap) (ty,def) in |
| 144 | + List.rev_map f gt.goal_hyps, |
| 145 | + Typ("?"^to_string int gt.goal_meta.meta_key, |
| 146 | + to_string term gt.goal_type) |
| 147 | + | Unif(c,t,u) -> |
| 148 | + let f (v,ty,def) = |
| 149 | + to_string var v, to_string (typ_or_def idmap) (ty,def) in |
| 150 | + List.rev_map f c, |
| 151 | + Unif(to_string term t^" ≡ "^to_string term u) |
| 152 | + |
| 153 | +(** [add_goals_of_problem p gs] extends the list of goals [gs] with the |
| 154 | + metavariables and constraints of [p]. *) |
| 155 | +let add_goals_of_problem : problem -> goal list -> goal list = fun p gs -> |
| 156 | + let gs = MetaSet.fold (fun m gs -> of_meta m :: gs) !p.metas gs in |
| 157 | + let f gs c = Unif c :: gs in |
| 158 | + let gs = List.fold_left f gs !p.to_solve in |
| 159 | + List.fold_left f gs !p.unsolved |
0 commit comments