made executable again

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

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 55516bf34aebd02241badb49501372493227f511..45fbe756aa2da62ec4c39d435f346e89bec51de0 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -68,8 +68,10 @@ type pattern  = C.annterm
 type body     = C.annterm option
 type types    = C.anninductiveType list
 type lpsno    = int
+type fields   = (string * bool * int) list
 
 type step = Note of note 
+          | Record of types * lpsno * fields * note
           | Inductive of types * lpsno * note
          | Statement of flavour * name * what * body * note
           | Qed of note
@@ -78,6 +80,7 @@ type step = Note of note
          | Intros of count option * name list * note
          | Cut of name * what * note
          | LetIn of name * what * note
+         | LApply of name * what * note
          | Rewrite of how * what * where * pattern * note
          | Elim of what * using option * pattern * note
          | Cases of what * pattern * note
@@ -134,7 +137,7 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_inductive types lpsno =
+let mk_pre_inductive types lpsno =
    let map1 (lps1, cons) (name, arity) = 
       let lps2, arity = strip_lps lpsno arity in
       merge_lps lps1 lps2, (name, arity) :: cons
@@ -146,13 +149,32 @@ let mk_inductive types lpsno =
    in
    let map3 (name, xw) = arel_of_name name, xw in
    let rev_lps, rev_types = List.fold_left map2 ([], []) types in
-   let lpars, types = List.rev_map map3 rev_lps, List.rev rev_types in
+   List.rev_map map3 rev_lps, List.rev rev_types
+
+let mk_inductive types lpsno =
+   let lpars, types = mk_pre_inductive types lpsno in
    let obj = N.Inductive (lpars, types) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
+let mk_record types lpsno fields =
+   match mk_pre_inductive types lpsno with
+      | lpars, [name, _, ty, [_, cty]] -> 
+         let map (fields, cty) (name, coercion, arity) =
+           match cty with
+              | C.AProd (_, _, w, t) ->
+                 (name, w, coercion, arity) :: fields, t
+              | _                    ->
+                 assert false
+        in
+        let rev_fields, _ = List.fold_left map ([], cty) fields in 
+        let fields = List.rev rev_fields in
+        let obj = N.Record (lpars, name, ty, fields) in
+         G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+      | _ -> assert false
+
 let mk_statement flavour name t v =
    let name = match name with Some name -> name | None -> assert false in
-   let obj = N.Theorem (flavour, name, t, v) in
+   let obj = N.Theorem (flavour, name, t, v, `Regular) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
 let mk_qed =
@@ -186,6 +208,10 @@ let mk_letin name what punctation =
    let tactic = G.LetIn (floc, what, name) in
    mk_tactic tactic punctation
 
+let mk_lapply name what punctation =
+   let tactic = G.LApply (floc, false, None, [], what, name) in
+   mk_tactic tactic punctation
+
 let mk_rewrite direction what where pattern punctation =
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
@@ -247,13 +273,15 @@ let mk_vb = G.Shift floc
 let rec render_step sep a = function
    | Note s                    -> mk_notenote s a
    | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a 
-   | Inductive (lps, ts, s)    -> mk_inductive lps ts :: mk_thnote s a
+   | Inductive (ts, lps, s)    -> mk_inductive ts lps :: mk_thnote s a
+   | Record (ts, lps, fs, s)   -> mk_record ts lps fs :: mk_thnote s a
    | Qed s                     -> mk_qed :: mk_tacnote s a
    | Exact (t, s)              -> mk_exact t sep :: mk_tacnote s a   
    | Id s                      -> mk_id sep :: mk_tacnote s a
    | Intros (c, ns, s)         -> mk_intros c ns sep :: mk_tacnote s a
    | Cut (n, t, s)             -> mk_cut n t sep :: mk_tacnote s a
    | LetIn (n, t, s)           -> mk_letin n t sep :: mk_tacnote s a
+   | LApply (n, t, s)          -> mk_lapply n t sep :: mk_tacnote s a
    | Rewrite (b, t, w, e, s)   -> mk_rewrite b t w e sep :: mk_tacnote s a
    | Elim (t, xu, e, s)        -> mk_elim t xu e sep :: mk_tacnote s a
    | Cases (t, e, s)           -> mk_cases t e sep :: mk_tacnote s a
@@ -310,6 +338,7 @@ let count = I.count_nodes ~meta:false
 
 let rec count_node a = function
    | Note _
+   | Record _
    | Inductive _
    | Statement _
    | Qed _   
@@ -321,6 +350,7 @@ let rec count_node a = function
    | Exact (t, _) 
    | Cut (_, t, _)
    | LetIn (_, t, _)
+   | LApply (_, t, _)
    | Apply (t, _)            -> count a (H.cic t)
    | Rewrite (_, t, _, p, _)
    | Elim (t, _, p, _)
@@ -336,12 +366,14 @@ let rec note_of_step = function
    | Note s
    | Statement (_, _, _, _, s)
    | Inductive (_, _, s)
+   | Record (_, _, _, s)
    | Qed s
    | Exact (_, s)
    | Id s
    | Intros (_, _, s)
    | Cut (_, _, s)
    | LetIn (_, _, s)
+   | LApply (_, _, s)
    | Rewrite (_, _, _, _, s)
    | Elim (_, _, _, s)
    | Cases (_, _, s)