From 8917ab003a9b7f2abf8e399b5e7ad013b31a2e0e Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 20 Sep 2012 09:41:14 +0200 Subject: Imported Upstream version 0.3 --- AAC_theory.ml | 1097 --------------------------------------------------------- 1 file changed, 1097 deletions(-) delete mode 100644 AAC_theory.ml (limited to 'AAC_theory.ml') diff --git a/AAC_theory.ml b/AAC_theory.ml deleted file mode 100644 index 55b9e21..0000000 --- a/AAC_theory.ml +++ /dev/null @@ -1,1097 +0,0 @@ -(***************************************************************************) -(* This is part of aac_tactics, it is distributed under the terms of the *) -(* GNU Lesser General Public License version 3 *) -(* (see file LICENSE for more details) *) -(* *) -(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) -(***************************************************************************) - -(** Constr from the theory of this particular development - - The inner-working of this module is highly correlated with the - particular structure of {b AAC.v}, therefore, it should - be of little interest to most readers. -*) -open Term - -module Control = struct - let printing = true - let debug = false - let time = false -end - -module Debug = AAC_helper.Debug (Control) -open Debug - -(** {1 HMap : Specialized Hashtables based on constr} *) - - -module Hashed_constr = -struct - type t = constr - let equal = (=) - let hash = Hashtbl.hash -end - - (* TODO module HMap = Hashtbl, du coup ? *) -module HMap = Hashtbl.Make(Hashed_constr) - -let ac_theory_path = ["AAC_tactics"; "AAC"] - -module Stubs = struct - let path = ac_theory_path@["Internal"] - - (** The constants from the inductive type *) - let _Tty = lazy (AAC_coq.init_constant path "T") - let vTty = lazy (AAC_coq.init_constant path "vT") - - let rsum = lazy (AAC_coq.init_constant path "sum") - let rprd = lazy (AAC_coq.init_constant path "prd") - let rsym = lazy (AAC_coq.init_constant path "sym") - let runit = lazy (AAC_coq.init_constant path "unit") - - let vnil = lazy (AAC_coq.init_constant path "vnil") - let vcons = lazy (AAC_coq.init_constant path "vcons") - let eval = lazy (AAC_coq.init_constant path "eval") - - - let decide_thm = lazy (AAC_coq.init_constant path "decide") - let lift_normalise_thm = lazy (AAC_coq.init_constant path "lift_normalise") - - let lift = - lazy (AAC_coq.init_constant ac_theory_path "AAC_lift") - let lift_proj_equivalence= - lazy (AAC_coq.init_constant ac_theory_path "aac_lift_equivalence") - let lift_transitivity_left = - lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_left") - let lift_transitivity_right = - lazy(AAC_coq.init_constant ac_theory_path "lift_transitivity_right") - let lift_reflexivity = - lazy(AAC_coq.init_constant ac_theory_path "lift_reflexivity") -end - -module Classes = struct - module Associative = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Associative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value - |] ) - let infer goal rlt value = - let ty = ty rlt value in - AAC_coq.resolve_one_typeclass goal ty - end - - module Commutative = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Commutative") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) = - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value - |] ) - - end - - module Proper = struct - let path = ac_theory_path @ ["Internal";"Sym"] - let typeof = lazy (AAC_coq.init_constant path "type_of") - let relof = lazy (AAC_coq.init_constant path "rel_of") - let mk_typeof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> - let x = rlt.AAC_coq.Relation.carrier in - mkApp (Lazy.force typeof, [| x ; AAC_coq.Nat.of_int n |]) - let mk_relof : AAC_coq.Relation.t -> int -> constr = fun rlt n -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force relof, [| x;r ; AAC_coq.Nat.of_int n |]) - - let ty rlt op ar = - let typeof = mk_typeof rlt ar in - let relof = mk_relof rlt ar in - AAC_coq.Classes.mk_morphism typeof relof op - let infer goal rlt op ar = - let ty = ty rlt op ar in - AAC_coq.resolve_one_typeclass goal ty - end - - module Unit = struct - let path = ac_theory_path - let typ = lazy (AAC_coq.init_constant path "Unit") - let ty (rlt : AAC_coq.Relation.t) (value : Term.constr) (unit : Term.constr)= - mkApp (Lazy.force typ, [| rlt.AAC_coq.Relation.carrier; - rlt.AAC_coq.Relation.r; - value; - unit - |] ) - end - -end - -(* Non empty lists *) -module NEList = struct - let path = ac_theory_path @ ["Internal"] - let typ = lazy (AAC_coq.init_constant path "list") - let nil = lazy (AAC_coq.init_constant path "nil") - let cons = lazy (AAC_coq.init_constant path "cons") - let cons ty h t = - mkApp (Lazy.force cons, [| ty; h ; t |]) - let nil ty x = - (mkApp (Lazy.force nil, [| ty ; x|])) - let rec of_list ty = function - | [] -> invalid_arg "NELIST" - | [x] -> nil ty x - | t::q -> cons ty t (of_list ty q) - - let type_of_list ty = - mkApp (Lazy.force typ, [|ty|]) -end - -(** a [mset] is a ('a * pos) list *) -let mk_mset ty (l : (constr * int) list) = - let pos = Lazy.force AAC_coq.Pos.typ in - let pair (x : constr) (ar : int) = - AAC_coq.Pair.of_pair ty pos (x, AAC_coq.Pos.of_int ar) - in - let pair_ty = AAC_coq.lapp AAC_coq.Pair.typ [| ty ; pos|] in - let rec aux = function - | [ ] -> assert false - | [x,ar] -> NEList.nil pair_ty (pair x ar) - | (t,ar)::q -> NEList.cons pair_ty (pair t ar) (aux q) - in - aux l - -module Sigma = struct - let sigma = lazy (AAC_coq.init_constant ac_theory_path "sigma") - let sigma_empty = lazy (AAC_coq.init_constant ac_theory_path "sigma_empty") - let sigma_add = lazy (AAC_coq.init_constant ac_theory_path "sigma_add") - let sigma_get = lazy (AAC_coq.init_constant ac_theory_path "sigma_get") - - let add ty n x map = - mkApp (Lazy.force sigma_add,[|ty; n; x ; map|]) - let empty ty = - mkApp (Lazy.force sigma_empty,[|ty |]) - let typ ty = - mkApp (Lazy.force sigma, [|ty|]) - - let to_fun ty null map = - mkApp (Lazy.force sigma_get, [|ty;null;map|]) - - let of_list ty null l = - match l with - | (_,t)::q -> - let map = - List.fold_left - (fun acc (i,t) -> - assert (i > 0); - add ty (AAC_coq.Pos.of_int i) ( t) acc) - (empty ty) - q - in to_fun ty (t) map - | [] -> debug "of_list empty" ; to_fun ty (null) (empty ty) - - -end - - -module Sym = struct - type pack = {ar: Term.constr; value: Term.constr ; morph: Term.constr} - let path = ac_theory_path @ ["Internal";"Sym"] - let typ = lazy (AAC_coq.init_constant path "pack") - let mkPack = lazy (AAC_coq.init_constant path "mkPack") - let value = lazy (AAC_coq.init_constant path "value") - let null = lazy (AAC_coq.init_constant path "null") - let mk_pack (rlt: AAC_coq.Relation.t) s = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force mkPack, [|x;r; s.ar;s.value;s.morph|]) - let null rlt = - let x = rlt.AAC_coq.Relation.carrier in - let r = rlt.AAC_coq.Relation.r in - mkApp (Lazy.force null, [| x;r;|]) - - let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force typ, [| x; r|] ) -end - -module Bin =struct - type pack = {value : Term.constr; - compat : Term.constr; - assoc : Term.constr; - comm : Term.constr option; - } - - let path = ac_theory_path @ ["Internal";"Bin"] - let typ = lazy (AAC_coq.init_constant path "pack") - let mkPack = lazy (AAC_coq.init_constant path "mk_pack") - - let mk_pack: AAC_coq.Relation.t -> pack -> Term.constr = fun (rlt) s -> - let (x,r) = AAC_coq.Relation.split rlt in - let comm_ty = Classes.Commutative.ty rlt s.value in - mkApp (Lazy.force mkPack , [| x ; r; - s.value; - s.compat ; - s.assoc; - AAC_coq.Option.of_option comm_ty s.comm - |]) - let mk_ty : AAC_coq.Relation.t -> constr = fun rlt -> - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force typ, [| x; r|] ) -end - -module Unit = struct - let path = ac_theory_path @ ["Internal"] - let unit_of_ty = lazy (AAC_coq.init_constant path "unit_of") - let unit_pack_ty = lazy (AAC_coq.init_constant path "unit_pack") - let mk_unit_of = lazy (AAC_coq.init_constant path "mk_unit_for") - let mk_unit_pack = lazy (AAC_coq.init_constant path "mk_unit_pack") - - type unit_of = - { - uf_u : Term.constr; (* u *) - uf_idx : Term.constr; - uf_desc : Term.constr; (* Unit R (e_bin uf_idx) u *) - } - - type pack = { - u_value : Term.constr; (* X *) - u_desc : (unit_of) list (* unit_of u_value *) - } - - let ty_unit_of rlt e_bin u = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp ( Lazy.force unit_of_ty, [| x; r; e_bin; u |]) - - let ty_unit_pack rlt e_bin = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force unit_pack_ty, [| x; r; e_bin |]) - - let mk_unit_of rlt e_bin u unit_of = - let (x,r) = AAC_coq.Relation.split rlt in - mkApp (Lazy.force mk_unit_of , [| x; - r; - e_bin ; - u; - unit_of.uf_idx; - unit_of.uf_desc - |]) - - let mk_pack rlt e_bin pack : Term.constr = - let (x,r) = AAC_coq.Relation.split rlt in - let ty = ty_unit_of rlt e_bin pack.u_value in - let mk_unit_of = mk_unit_of rlt e_bin pack.u_value in - let u_desc =AAC_coq.List.of_list ( ty ) (List.map mk_unit_of pack.u_desc) in - mkApp (Lazy.force mk_unit_pack, [|x;r; - e_bin ; - pack.u_value; - u_desc - |]) - - let default x : pack = - { u_value = x; - u_desc = [] - } - -end - -let anomaly msg = - Util.anomaly ("aac_tactics: " ^ msg) - -let user_error msg = - Util.error ("aac_tactics: " ^ msg) - -module Trans = struct - - (** {1 From Coq to Abstract Syntax Trees (AST)} - - This module provides facilities to interpret a Coq term with - arbitrary operators as an abstract syntax tree. Considering an - application, we try to infer instances of our classes. - - We consider that [A] operators are coarser than [AC] operators, - which in turn are coarser than raw morphisms. That means that - [List.append], of type [(A : Type) -> list A -> list A -> list - A] can be understood as an [A] operator. - - During this reification, we gather some informations that will - be used to rebuild Coq terms from AST ( type {!envs}) - - We use a main hash-table from [constr] to [pack], in order to - discriminate the various constructors. All these are mixed in - order to improve on the number of comparisons in the tables *) - - (* 'a * (unit, op_unit) option *) - type 'a with_unit = 'a * (Unit.unit_of) option - type pack = - (* used to infer the AC/A structure in the first pass {!Gather} *) - | Bin of Bin.pack with_unit - (* will only be used in the second pass : {!Parse}*) - | Sym of Sym.pack - | Unit of constr (* to avoid confusion in bloom *) - - (** discr is a map from {!Term.constr} to {!pack}. - - [None] means that it is not possible to instantiate this partial - application to an interesting class. - - [Some x] means that we found something in the past. This means - in particular that a single [constr] cannot be two things at the - same time. - - The field [bloom] allows to give a unique number to each class we - found. *) - type envs = - { - discr : (pack option) HMap.t ; - bloom : (pack, int ) Hashtbl.t; - bloom_back : (int, pack ) Hashtbl.t; - bloom_next : int ref; - } - - let empty_envs () = - { - discr = HMap.create 17; - bloom = Hashtbl.create 17; - bloom_back = Hashtbl.create 17; - bloom_next = ref 1; - } - - - - let add_bloom envs pack = - if Hashtbl.mem envs.bloom pack - then () - else - let x = ! (envs.bloom_next) in - Hashtbl.add envs.bloom pack x; - Hashtbl.add envs.bloom_back x pack; - incr (envs.bloom_next) - - let find_bloom envs pack = - try Hashtbl.find envs.bloom pack - with Not_found -> assert false - - (********************************************) - (* (\* Gather the occuring AC/A symbols *\) *) - (********************************************) - - (** This modules exhibit a function that memoize in the environment - all the AC/A operators as well as the morphism that occur. This - staging process allows us to prefer AC/A operators over raw - morphisms. Moreover, for each AC/A operators, we need to try to - infer units. Otherwise, we do not have [x * y * x <= a * a] since 1 - does not occur. - - But, do we also need to check whether constants are - units. Otherwise, we do not have the ability to rewrite [0 = a + - a] in [a = ...]*) - module Gather : sig - val gather : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> Term.constr -> AAC_coq.goal_sigma - end - = struct - - let memoize envs t pack : unit = - begin - HMap.add envs.discr t (Some pack); - add_bloom envs pack; - match pack with - | Bin (_, None) | Sym _ -> () - | Bin (_, Some (unit_of)) -> - let unit = unit_of.Unit.uf_u in - HMap.add envs.discr unit (Some (Unit unit)); - add_bloom envs (Unit unit); - | Unit _ -> assert false - end - - - let get_unit (rlt : AAC_coq.Relation.t) op goal : - (AAC_coq.goal_sigma * constr * constr ) option= - let x = (rlt.AAC_coq.Relation.carrier) in - let unit, goal = AAC_coq.evar_unit goal x in - let ty =Classes.Unit.ty rlt op unit in - let result = - try - let t,goal = AAC_coq.resolve_one_typeclass goal ty in - Some (goal,t,unit) - with Not_found -> None - in - match result with - | None -> None - | Some (goal,s,unit) -> - let unit = AAC_coq.nf_evar goal unit in - Some (goal, unit, s) - - - - (** gives back the class and the operator *) - let is_bin (rlt: AAC_coq.Relation.t) (op: constr) ( goal: AAC_coq.goal_sigma) - : (AAC_coq.goal_sigma * Bin.pack) option = - let assoc_ty = Classes.Associative.ty rlt op in - let comm_ty = Classes.Commutative.ty rlt op in - let proper_ty = Classes.Proper.ty rlt op 2 in - try - let proper , goal = AAC_coq.resolve_one_typeclass goal proper_ty in - let assoc, goal = AAC_coq.resolve_one_typeclass goal assoc_ty in - let comm , goal = - try - let comm, goal = AAC_coq.resolve_one_typeclass goal comm_ty in - Some comm, goal - with Not_found -> - None, goal - in - let bin = - {Bin.value = op; - Bin.compat = proper; - Bin.assoc = assoc; - Bin.comm = comm } - in - Some (goal,bin) - with |Not_found -> None - - let is_bin (rlt : AAC_coq.Relation.t) (op : constr) (goal : AAC_coq.goal_sigma)= - match is_bin rlt op goal with - | None -> None - | Some (goal, bin_pack) -> - match get_unit rlt op goal with - | None -> Some (goal, Bin (bin_pack, None)) - | Some (gl, unit,s) -> - let unit_of = - { - Unit.uf_u = unit; - (* TRICK : this term is not well-typed by itself, - but it is okay the way we use it in the other - functions *) - Unit.uf_idx = op; - Unit.uf_desc = s; - } - in Some (gl,Bin (bin_pack, Some (unit_of))) - - - (** {is_morphism} try to infer the kind of operator we are - dealing with *) - let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in - let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try - let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with - | Not_found -> None - - - (* [crop_app f [| a_0 ; ... ; a_n |]] - returns Some (f a_0 ... a_(n-2), [|a_(n-1); a_n |] ) - *) - let crop_app t ca : (constr * constr array) option= - let n = Array.length ca in - if n <= 1 - then None - else - let papp = Term.mkApp (t, Array.sub ca 0 (n-2) ) in - let args = Array.sub ca (n-2) 2 in - Some (papp, args ) - - let fold goal (rlt : AAC_coq.Relation.t) envs t ca cont = - let fold_morphism t ca = - let nb_params = Array.length ca in - let rec aux n = - assert (n < nb_params && 0 < nb_params ); - let papp = Term.mkApp (t, Array.sub ca 0 n) in - match is_morphism goal rlt papp (nb_params - n) with - | None -> - (* here we have to memoize the failures *) - HMap.add envs.discr papp None; - if n < nb_params - 1 then aux (n+1) else goal - | Some (goal, pack) -> - let args = Array.sub ca (n) (nb_params -n)in - let goal = Array.fold_left cont goal args in - memoize envs papp pack; - goal - in - if nb_params = 0 then goal else aux 0 - in - let is_aac t = is_bin rlt t in - match crop_app t ca with - | None -> - fold_morphism t ca - | Some (papp, args) -> - begin match is_aac papp goal with - | None -> fold_morphism t ca - | Some (goal, pack) -> - memoize envs papp pack; - Array.fold_left cont goal args - end - - (* update in place the envs of known stuff, using memoization. We - have to memoize failures, here. *) - let gather goal (rlt : AAC_coq.Relation.t ) envs t : AAC_coq.goal_sigma = - let rec aux goal x = - match AAC_coq.decomp_term x with - | App (t,ca) -> - fold goal rlt envs t ca (aux ) - | _ -> goal - in - aux goal t - end - - (** We build a term out of a constr, updating in place the - environment if needed (the only kind of such updates are the - constants). *) - module Parse : - sig - val t_of_constr : AAC_coq.goal_sigma -> AAC_coq.Relation.t -> envs -> constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma - end - = struct - - (** [discriminates goal envs rlt t ca] infer : - - - its {! pack } (is it an AC operator, or an A operator, or a - Symbol ?), - - - the relevant partial application, - - - the vector of the remaining arguments - - We use an expansion to handle the special case of units, - before going back to the general discrimination - procedure. That means that a unit is more coarse than a raw - morphism - - This functions is prevented to go through [ar < 0] by the fact - that a constant is a morphism. But not an eva. *) - - let is_morphism goal (rlt : AAC_coq.Relation.t) (papp : Term.constr) (ar : int) : (AAC_coq.goal_sigma * pack ) option = - let typeof = Classes.Proper.mk_typeof rlt ar in - let relof = Classes.Proper.mk_relof rlt ar in - let m = AAC_coq.Classes.mk_morphism typeof relof papp in - try - let m,goal = AAC_coq.resolve_one_typeclass goal m in - let pack = {Sym.ar = (AAC_coq.Nat.of_int ar); Sym.value= papp; Sym.morph= m} in - Some (goal, Sym pack) - with - | e -> None - - exception NotReflexive - let discriminate goal envs (rlt : AAC_coq.Relation.t) t ca : AAC_coq.goal_sigma * pack * constr * constr array = - let nb_params = Array.length ca in - let rec fold goal ar :AAC_coq.goal_sigma * pack * constr * constr array = - begin - assert (0 <= ar && ar <= nb_params); - let p_app = mkApp (t, Array.sub ca 0 (nb_params - ar)) in - begin - try - begin match HMap.find envs.discr p_app with - | None -> - fold goal (ar-1) - | Some pack -> - (goal, pack, p_app, Array.sub ca (nb_params -ar ) ar) - end - with - Not_found -> (* Could not find this constr *) - memoize (is_morphism goal rlt p_app ar) p_app ar - end - end - and memoize (x) p_app ar = - assert (0 <= ar && ar <= nb_params); - match x with - | Some (goal, pack) -> - HMap.add envs.discr p_app (Some pack); - add_bloom envs pack; - (goal, pack, p_app, Array.sub ca (nb_params-ar) ar) - | None -> - - if ar = 0 then raise NotReflexive; - begin - (* to memoise the failures *) - HMap.add envs.discr p_app None; - (* will terminate, since [const] is capped, and it is - easy to find an instance of a constant *) - fold goal (ar-1) - end - in - try match HMap.find envs.discr (mkApp (t,ca))with - | None -> fold goal (nb_params) - | Some pack -> goal, pack, (mkApp (t,ca)), [| |] - with Not_found -> fold goal (nb_params) - - let discriminate goal envs rlt x = - try - match AAC_coq.decomp_term x with - | App (t,ca) -> - discriminate goal envs rlt t ca - | _ -> discriminate goal envs rlt x [| |] - with - | NotReflexive -> user_error "The relation to which the goal was lifted is not Reflexive" - (* TODO: is it the only source of invalid use that fall - into this catch_all ? *) - | e -> - user_error "Cannot handle this kind of hypotheses (variables occuring under a function symbol which is not a proper morphism)." - - (** [t_of_constr goal rlt envs cstr] builds the abstract syntax tree - of the term [cstr]. Doing so, it modifies the environment of - known stuff [envs], and eventually creates fresh - evars. Therefore, we give back the goal updated accordingly *) - let t_of_constr goal (rlt: AAC_coq.Relation.t ) envs : constr -> AAC_matcher.Terms.t * AAC_coq.goal_sigma = - let r_goal = ref (goal) in - let rec aux x = - match AAC_coq.decomp_term x with - | Rel i -> AAC_matcher.Terms.Var i - | _ -> - let goal, pack , p_app, ca = discriminate (!r_goal) envs rlt x in - r_goal := goal; - let k = find_bloom envs pack - in - match pack with - | Bin (pack,_) -> - begin match pack.Bin.comm with - | Some _ -> - assert (Array.length ca = 2); - AAC_matcher.Terms.Plus ( k, aux ca.(0), aux ca.(1)) - | None -> - assert (Array.length ca = 2); - AAC_matcher.Terms.Dot ( k, aux ca.(0), aux ca.(1)) - end - | Unit _ -> - assert (Array.length ca = 0); - AAC_matcher.Terms.Unit ( k) - | Sym _ -> - AAC_matcher.Terms.Sym ( k, Array.map aux ca) - in - ( - fun x -> let r = aux x in r, !r_goal - ) - - end (* Parse *) - - let add_symbol goal rlt envs l = - let goal = Gather.gather goal rlt envs (Term.mkApp (l, [| Term.mkRel 0;Term.mkRel 0|])) in - goal - - (* [t_of_constr] buils a the abstract syntax tree of a constr, - updating in place the environment. Doing so, we infer all the - morphisms and the AC/A operators. It is mandatory to do so both - for the pattern and the term, since AC symbols can occur in one - and not the other *) - let t_of_constr goal rlt envs (l,r) = - let goal = Gather.gather goal rlt envs l in - let goal = Gather.gather goal rlt envs r in - let l,goal = Parse.t_of_constr goal rlt envs l in - let r, goal = Parse.t_of_constr goal rlt envs r in - l, r, goal - - (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *) - - type ir = - { - packer : (int, pack) Hashtbl.t; (* = bloom_back *) - bin : (int * Bin.pack) list ; - units : (int * Unit.pack) list; - sym : (int * Term.constr) list ; - matcher_units : AAC_matcher.ext_units - } - - let ir_to_units ir = ir.matcher_units - - let ir_of_envs goal (rlt : AAC_coq.Relation.t) envs = - let add x y l = (x,y)::l in - let nil = [] in - let sym , - (bin : (int * Bin.pack with_unit) list), - (units : (int * constr) list) = - Hashtbl.fold - (fun int pack (sym,bin,units) -> - match pack with - | Bin s -> - sym, add (int) s bin, units - | Sym s -> - add (int) s sym, bin, units - | Unit s -> - sym, bin, add int s units - ) - envs.bloom_back - (nil,nil,nil) - in - let matcher_units = - let unit_for , is_ac = - List.fold_left - (fun ((unit_for,is_ac) as acc) (n,(bp,wu)) -> - match wu with - | None -> acc - | Some (unit_of) -> - let unit_n = Hashtbl.find envs.bloom - (Unit unit_of.Unit.uf_u) - in - ( n, unit_n)::unit_for, - (n, bp.Bin.comm <> None )::is_ac - - ) - ([],[]) bin - in - {AAC_matcher.unit_for = unit_for; AAC_matcher.is_ac = is_ac} - - in - let units : (int * Unit.pack) list = - List.fold_left - (fun acc (n,u) -> - (* first, gather all bins with this unit *) - let all_bin = - List.fold_left - ( fun acc (nop,(bp,wu)) -> - match wu with - | None -> acc - | Some unit_of -> - if unit_of.Unit.uf_u = u - then - {unit_of with - Unit.uf_idx = (AAC_coq.Pos.of_int nop)} :: acc - else - acc - ) - [] bin - in - (n,{ - Unit.u_value = u; - Unit.u_desc = all_bin - })::acc - ) - [] units - - in - goal, { - packer = envs.bloom_back; - bin = (List.map (fun (n,(s,_)) -> n, s) bin); - units = units; - sym = (List.map (fun (n,s) -> n,(Sym.mk_pack rlt s)) sym); - matcher_units = matcher_units - } - - - - (** {1 From AST back to Coq } - - The next functions allow one to map OCaml abstract syntax trees - to Coq terms *) - - (** {2 Building raw, natural, terms} *) - - (** [raw_constr_of_t_debruijn] rebuilds a term in the raw - representation, without products on top, and maybe escaping free - debruijn indices (in the case of a pattern for example). *) - let raw_constr_of_t_debruijn ir (t : AAC_matcher.Terms.t) : Term.constr * int list = - let add_set,get = - let r = ref [] in - let rec add x = function - [ ] -> [x] - | t::q when t = x -> t::q - | t::q -> t:: (add x q) - in - (fun x -> r := add x !r),(fun () -> !r) - in - (* Here, we rely on the invariant that the maps are well formed: - it is meanigless to fail to find a symbol in the maps, or to - find the wrong kind of pack in the maps *) - let rec aux t = - match t with - | AAC_matcher.Terms.Plus (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> - mkApp (s.Bin.value , [|(aux l);(aux r)|]) - | _ -> Printf.printf "erreur:%i\n%!"s; - assert false - end - | AAC_matcher.Terms.Dot (s,l,r) -> - begin match Hashtbl.find ir.packer s with - | Bin (s,_) -> - mkApp (s.Bin.value, [|(aux l);(aux r)|]) - | _ -> assert false - end - | AAC_matcher.Terms.Sym (s,t) -> - begin match Hashtbl.find ir.packer s with - | Sym s -> - mkApp (s.Sym.value, Array.map aux t) - | _ -> assert false - end - | AAC_matcher.Terms.Unit x -> - begin match Hashtbl.find ir.packer x with - | Unit s -> s - | _ -> assert false - end - | AAC_matcher.Terms.Var i -> add_set i; - mkRel (i) - in - let t = aux t in - t , get ( ) - - (** [raw_constr_of_t] rebuilds a term in the raw representation *) - let raw_constr_of_t ir rlt (context:rel_context) t = - (** cap rebuilds the products in front of the constr *) - let rec cap c = function [] -> c - | t::q -> - let i = Term.lookup_rel t context in - cap (mkProd_or_LetIn i c) q - in - let t,indices = raw_constr_of_t_debruijn ir t in - cap t (List.sort (Pervasives.compare) indices) - - - (** {2 Building reified terms} *) - - (* Some informations to be able to build the maps *) - type reif_params = - { - bin_null : Bin.pack; (* the default A operator *) - sym_null : constr; - unit_null : Unit.pack; - sym_ty : constr; (* the type, as it appears in e_sym *) - bin_ty : constr - } - - - (** A record containing the environments that will be needed by the - decision procedure, as a Coq constr. Contains the functions - from the symbols (as ints) to indexes (as constr) *) - - type sigmas = { - env_sym : Term.constr; - env_bin : Term.constr; - env_units : Term.constr; (* the [idx -> X:constr] *) - } - - - type sigma_maps = { - sym_to_pos : int -> Term.constr; - bin_to_pos : int -> Term.constr; - units_to_pos : int -> Term.constr; - } - - - (** infers some stuff that will be required when we will build - environments (our environments need a default case, so we need - an Op_AC, an Op_A, and a symbol) *) - (* Note : this function can fail if the user is using the wrong - relation, like proving a = b, while the classes are defined with - another relation (==) *) - let build_reif_params goal (rlt : AAC_coq.Relation.t) (zero) : - reif_params * AAC_coq.goal_sigma = - let carrier = rlt.AAC_coq.Relation.carrier in - let bin_null = - try - let op,goal = AAC_coq.evar_binary goal carrier in - let assoc,goal = Classes.Associative.infer goal rlt op in - let compat,goal = Classes.Proper.infer goal rlt op 2 in - let op = AAC_coq.nf_evar goal op in - { - Bin.value = op; - Bin.compat = compat; - Bin.assoc = assoc; - Bin.comm = None - } - with Not_found -> user_error "Cannot infer a default A operator (required at least to be Proper and Associative)" - in - let zero, goal = - try - let evar_op,goal = AAC_coq.evar_binary goal carrier in - let evar_unit, goal = AAC_coq.evar_unit goal carrier in - let query = Classes.Unit.ty rlt evar_op evar_unit in - let _, goal = AAC_coq.resolve_one_typeclass goal query in - AAC_coq.nf_evar goal evar_unit, goal - with _ -> zero, goal in - let sym_null = Sym.null rlt in - let unit_null = Unit.default zero in - let record = - { - bin_null = bin_null; - sym_null = sym_null; - unit_null = unit_null; - sym_ty = Sym.mk_ty rlt ; - bin_ty = Bin.mk_ty rlt - } - in - record, goal - - (* We want to lift down the indexes of symbols. *) - let renumber (l: (int * 'a) list ) = - let _, l = List.fold_left (fun (next,acc) (glob,x) -> - (next+1, (next,glob,x)::acc) - ) (1,[]) l - in - let rec to_global loc = function - | [] -> assert false - | (local, global,x)::q when local = loc -> global - | _::q -> to_global loc q - in - let rec to_local glob = function - | [] -> assert false - | (local, global,x)::q when global = glob -> local - | _::q -> to_local glob q - in - let locals = List.map (fun (local,global,x) -> local,x) l in - locals, (fun x -> to_local x l) , (fun x -> to_global x l) - - (** [build_sigma_maps] given a envs and some reif_params, we are - able to build the sigmas *) - let build_sigma_maps (rlt : AAC_coq.Relation.t) zero ir (k : sigmas * sigma_maps -> Proof_type.tactic ) : Proof_type.tactic = fun goal -> - let rp,goal = build_reif_params goal rlt zero in - let renumbered_sym, to_local, to_global = renumber ir.sym in - let env_sym = Sigma.of_list - rp.sym_ty - (rp.sym_null) - renumbered_sym - in - AAC_coq.cps_mk_letin "env_sym" env_sym - (fun env_sym -> - let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in - let env_bin = - Sigma.of_list - rp.bin_ty - (Bin.mk_pack rlt rp.bin_null) - bin - in - AAC_coq.cps_mk_letin "env_bin" env_bin - (fun env_bin -> - let units = (List.map (fun (n,s) -> n, Unit.mk_pack rlt env_bin s)ir.units) in - let env_units = - Sigma.of_list - (Unit.ty_unit_pack rlt env_bin) - (Unit.mk_pack rlt env_bin rp.unit_null ) - units - in - - AAC_coq.cps_mk_letin "env_units" env_units - (fun env_units -> - let sigmas = - { - env_sym = env_sym ; - env_bin = env_bin ; - env_units = env_units; - } in - let f = List.map (fun (x,_) -> (x,AAC_coq.Pos.of_int x)) in - let sigma_maps = - { - sym_to_pos = (let sym = f renumbered_sym in fun x -> (List.assoc (to_local x) sym)); - bin_to_pos = (let bin = f bin in fun x -> (List.assoc x bin)); - units_to_pos = (let units = f units in fun x -> (List.assoc x units)); - } - in - k (sigmas, sigma_maps ) - ) - ) - ) goal - - (** builders for the reification *) - type reif_builders = - { - rsum: constr -> constr -> constr -> constr; - rprd: constr -> constr -> constr -> constr; - rsym: constr -> constr array -> constr; - runit : constr -> constr - } - - (* donne moi une tactique, je rajoute ma part. Potentiellement, il - est possible d'utiliser la notation 'do' a la Haskell: - http://www.cas.mcmaster.ca/~carette/pa_monad/ *) - let (>>) : 'a * Proof_type.tactic -> ('a -> 'b * Proof_type.tactic) -> 'b * Proof_type.tactic = - fun (x,t) f -> - let b,t' = f x in - b, Tacticals.tclTHEN t t' - - let return x = x, Tacticals.tclIDTAC - - let mk_vect vnil vcons v = - let ar = Array.length v in - let rec aux = function - | 0 -> vnil - | n -> let n = n-1 in - mkApp( vcons, - [| - (AAC_coq.Nat.of_int n); - v.(ar - 1 - n); - (aux (n)) - |] - ) - in aux ar - - (* TODO: use a do notation *) - let mk_reif_builders (rlt: AAC_coq.Relation.t) (env_sym:constr) (k: reif_builders -> Proof_type.tactic) = - let x = (rlt.AAC_coq.Relation.carrier) in - let r = (rlt.AAC_coq.Relation.r) in - - let x_r_env = [|x;r;env_sym|] in - let tty = mkApp (Lazy.force Stubs._Tty, x_r_env) in - let rsum = mkApp (Lazy.force Stubs.rsum, x_r_env) in - let rprd = mkApp (Lazy.force Stubs.rprd, x_r_env) in - let rsym = mkApp (Lazy.force Stubs.rsym, x_r_env) in - let vnil = mkApp (Lazy.force Stubs.vnil, x_r_env) in - let vcons = mkApp (Lazy.force Stubs.vcons, x_r_env) in - AAC_coq.cps_mk_letin "tty" tty - (fun tty -> - AAC_coq.cps_mk_letin "rsum" rsum - (fun rsum -> - AAC_coq.cps_mk_letin "rprd" rprd - (fun rprd -> - AAC_coq.cps_mk_letin "rsym" rsym - (fun rsym -> - AAC_coq.cps_mk_letin "vnil" vnil - (fun vnil -> - AAC_coq.cps_mk_letin "vcons" vcons - (fun vcons -> - let r ={ - rsum = - begin fun idx l r -> - mkApp (rsum, [| idx ; mk_mset tty [l,1 ; r,1]|]) - end; - rprd = - begin fun idx l r -> - let lst = NEList.of_list tty [l;r] in - mkApp (rprd, [| idx; lst|]) - end; - rsym = - begin fun idx v -> - let vect = mk_vect vnil vcons v in - mkApp (rsym, [| idx; vect|]) - end; - runit = fun idx -> (* could benefit of a letin *) - mkApp (Lazy.force Stubs.runit , [|x;r;env_sym;idx; |]) - } - in k r - )))))) - - - - type reifier = sigma_maps * reif_builders - - - let mk_reifier rlt zero envs (k : sigmas *reifier -> Proof_type.tactic) = - build_sigma_maps rlt zero envs - (fun (s,sm) -> - mk_reif_builders rlt s.env_sym - (fun rb ->k (s,(sm,rb)) ) - - ) - - (** [reif_constr_of_t reifier t] rebuilds the term [t] in the - reified form. We use the [reifier] to minimise the size of the - terms (we make as much lets as possible)*) - let reif_constr_of_t (sm,rb) (t:AAC_matcher.Terms.t) : constr = - let rec aux = function - | AAC_matcher.Terms.Plus (s,l,r) -> - let idx = sm.bin_to_pos s in - rb.rsum idx (aux l) (aux r) - | AAC_matcher.Terms.Dot (s,l,r) -> - let idx = sm.bin_to_pos s in - rb.rprd idx (aux l) (aux r) - | AAC_matcher.Terms.Sym (s,t) -> - let idx = sm.sym_to_pos s in - rb.rsym idx (Array.map aux t) - | AAC_matcher.Terms.Unit s -> - let idx = sm.units_to_pos s in - rb.runit idx - | AAC_matcher.Terms.Var i -> - anomaly "call to reif_constr_of_t on a term with variables." - in aux t -end - - - -- cgit v1.2.3