- hExtlib: new function "list_assoc_all"

[helm.git] / helm / software / components / acic_procedural / procedural2.ml

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index f8007d3fc93b204c1fff97b5e0659d1d50245363..958fc4abbd0f80b5db55d89c48872193859260b0 100644 (file)
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -30,7 +30,6 @@ module TC   = CicTypeChecker
 module Un   = CicUniv
 module UM   = UriManager
 module Obj  = LibraryObjects
-module HObj = HelmLibraryObjects
 module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
@@ -40,6 +39,7 @@ module HEL  = HExtlib
 module DTI  = DoubleTypeInference
 module NU   = CicNotationUtil
 module L    = Librarian
+module G    = GrafiteAst
 
 module Cl   = ProceduralClassify
 module T    = ProceduralTypes
@@ -47,12 +47,14 @@ module Cn   = ProceduralConversion
 module H    = ProceduralHelpers
 
 type status = {
-   sorts : (C.id, A.sort_kind) Hashtbl.t;
-   types : (C.id, A.anntypes) Hashtbl.t;
+   sorts    : (C.id, A.sort_kind) Hashtbl.t;
+   types    : (C.id, A.anntypes) Hashtbl.t;
+   params   : G.inline_param list;
    max_depth: int option;
-   depth: int;
-   context: C.context;
-   case: int list
+   depth    : int;
+   defaults : bool;
+   context  : C.context;
+   case     : int list
 }
 
 let debug = ref false
@@ -109,24 +111,22 @@ try
       | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
 with Invalid_argument _ -> failwith "A2P.test_depth"
 
-let is_rewrite_right = function
-   | C.AConst (_, uri, []) ->
-      UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
+let is_rewrite_right st = function
+   | C.AConst (_, uri, []) -> st.defaults && Obj.is_eq_ind_r_URI uri
    | _                     -> false
 
-let is_rewrite_left = function
-   | C.AConst (_, uri, []) ->
-      UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
+let is_rewrite_left st = function
+   | C.AConst (_, uri, []) -> st.defaults && Obj.is_eq_ind_URI uri
    | _                     -> false
 
-let is_fwd_rewrite_right hd tl =
-   if is_rewrite_right hd then match List.nth tl 3 with
+let is_fwd_rewrite_right st hd tl =
+   if is_rewrite_right st hd then match List.nth tl 3 with
       | C.ARel _ -> true
       | _        -> false
    else false
 
-let is_fwd_rewrite_left hd tl =
-   if is_rewrite_left hd then match List.nth tl 3 with
+let is_fwd_rewrite_left st hd tl =
+   if is_rewrite_left st hd then match List.nth tl 3 with
       | C.ARel _ -> true
       | _        -> false
    else false
@@ -291,11 +291,11 @@ and proc_letin st what name v w t =
       let st, hyp, rqv = match get_inner_types st v with
          | Some (ity, _) ->
            let st, rqv = match v with
-               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right hd tl ->
+               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl ->
                  mk_fwd_rewrite st dtext intro tl true v t ity
-              | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
+              | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left st hd tl  ->
                  mk_fwd_rewrite st dtext intro tl false v t ity
-              | v                                                     ->
+              | v                                                        ->
                  assert (Ut.is_sober st.context (H.cic ity));
                  let ity = H.acic_bc st.context ity in
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
@@ -365,9 +365,9 @@ and proc_appl st what hd tl =
               let qs = proc_bkd_proofs (next st) synth [] classes tl in
               let b, hd = mk_exp_args hd tl classes synth in
               script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")]
-           else if is_rewrite_right hd then 
+           else if is_rewrite_right st hd then 
               script2 @ mk_rewrite st dtext where qs tl2 false what
-           else if is_rewrite_left hd then 
+           else if is_rewrite_left st hd then 
               script2 @ mk_rewrite st dtext where qs tl2 true what
            else
               let predicate = List.nth tl2 (parsno - i) in
@@ -462,22 +462,26 @@ with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
 
 let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
 
-let def_flavours = [`Definition]
+let def_flavours = [`Definition; `Variant]
 
-let get_flavour ?flavour st v attrs =
+let get_flavour st v attrs =
    let rec aux = function
       | []               -> 
          if is_proof st v then List.hd th_flavours else List.hd def_flavours
       | `Flavour fl :: _ -> fl
       | _ :: tl          -> aux tl
    in
-   match flavour with
+   let flavour_map x y = match x, y with
+      | None, G.IPAs flavour -> Some flavour
+      | _                    -> x
+   in   
+   match List.fold_left flavour_map None st.params with
       | Some fl -> fl
       | None    -> aux attrs
 
-let proc_obj ?flavour ?(info="") st = function
+let proc_obj ?(info="") st = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
-      begin match get_flavour ?flavour st v attrs with
+      begin match get_flavour st v attrs with
          | flavour when List.mem flavour th_flavours  ->
             let ast = proc_proof st v in
             let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
@@ -497,12 +501,18 @@ let proc_obj ?flavour ?(info="") st = function
    | _                                          ->
       failwith "not a theorem, definition, axiom or inductive type"
 
-let init ~ids_to_inner_sorts ~ids_to_inner_types ?depth context =
+let init ~ids_to_inner_sorts ~ids_to_inner_types params context =
+   let depth_map x y = match x, y with
+      | None, G.IPDepth depth -> Some depth
+      | _                     -> x
+   in
    {
       sorts       = ids_to_inner_sorts;
       types       = ids_to_inner_types;
-      max_depth   = depth;
+      params      = params;
+      max_depth   = List.fold_left depth_map None params;
       depth       = 0;
+      defaults    = not (List.mem G.IPNoDefaults params);
       context     = context;
       case        = []
    }