X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=45fbe756aa2da62ec4c39d435f346e89bec51de0;hb=HEAD;hp=b30d6e86255c76486d85e0ce2c675bb7d162796d;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index b30d6e862..45fbe756a 100644
--- 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
@@ -86,6 +89,7 @@ type step = Note of note
 	  | Clear of hyp list * note
 	  | ClearBody of hyp * note
 	  | Branch of step list list * note
+          | Reflexivity of note
 
 (* annterm constructors *****************************************************)
 
@@ -133,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
@@ -145,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 =
@@ -185,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
@@ -206,7 +233,7 @@ let mk_cases what pattern punctation =
    mk_tactic tactic punctation
 
 let mk_apply t punctation =
-   let tactic = G.ApplyP (floc, t) in
+   let tactic = G.Apply (floc, t) in
    mk_tactic tactic punctation
 
 let mk_change t where pattern punctation =
@@ -225,6 +252,10 @@ let mk_clearbody id punctation =
    let tactic = G.ClearBody (floc, id) in
    mk_tactic tactic punctation
 
+let mk_reflexivity punctation =
+   let tactic = G.Reflexivity floc in
+   mk_tactic tactic punctation
+
 let mk_ob = 
    let punctation = G.Branch floc in
    mk_punctation punctation
@@ -242,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
@@ -258,10 +291,11 @@ let rec render_step sep a = function
    | ClearBody (n, s)          -> mk_clearbody n sep :: mk_tacnote s a
    | Branch ([], s)            -> a
    | Branch ([ps], s)          -> render_steps sep a ps
-   | Branch (ps :: pss, s)     ->      
+   | Branch (ps :: pss, s)     ->
       let a = mk_ob :: mk_tacnote s a in
       let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in
       mk_punctation sep :: render_steps mk_cb a ps
+   | Reflexivity s             -> mk_reflexivity sep :: mk_tacnote s a
 
 and render_steps sep a = function
    | []                                          -> a
@@ -281,16 +315,21 @@ let rec count_step a = function
    | Note _
    | Statement _
    | Inductive _
-   | Qed _
-(* level 0 *)   
-   | Intros (Some 0, [], _)
+   | Qed _                  -> a
+(* level A0 *)   
+   | Branch (pps, _)        -> List.fold_left count_steps a pps
+   | Clear _
+   | ClearBody _
    | Id _
+   | Intros (Some 0, [], _)
+(* leval A1 *)   
    | Exact _
-   | Change _
-   | Clear _
-   | ClearBody _            -> a
-   | Branch (pps, _)        -> List.fold_left count_steps a pps
-(* level 1 *)   
+(* level B1 *)   
+   | Cut _
+   | LetIn _
+(* level B2 *)   
+   | Change _               -> a
+(* level C *)   
    | _                      -> succ a   
 
 and count_steps a = List.fold_left count_step a
@@ -299,9 +338,11 @@ let count = I.count_nodes ~meta:false
 
 let rec count_node a = function
    | Note _
+   | Record _
    | Inductive _
    | Statement _
    | Qed _   
+   | Reflexivity _
    | Id _
    | Intros _
    | Clear _
@@ -309,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, _)
@@ -317,3 +359,27 @@ let rec count_node a = function
    | Branch (ss, _)          -> List.fold_left count_nodes a ss
 
 and count_nodes a = List.fold_left count_node a
+
+(* helpers ******************************************************************)
+
+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)
+   | Apply (_, s)
+   | Change (_, _, _, _, s)
+   | Clear (_, s)
+   | ClearBody (_, s)
+   | Reflexivity s
+   | Branch (_, s)             -> s