made executable again

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 68c88496ba91fbfe3e735a0264f2eb9be266b166..63b4d4972281d0c5f5822cf4555ee54b86ff56ee 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -57,6 +57,11 @@ let get_flavour sorts params context v attrs =
       | Some fl -> fl
       | None    -> aux attrs
 
+let rec is_record = function
+   | []                           -> None
+   | `Class (`Record fields) :: _ -> Some fields
+   | _ :: tl                      -> is_record tl
+
 let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, Some v, t, [], attrs)         ->
       begin match get_flavour sorts params context v attrs with
@@ -79,7 +84,10 @@ let proc_obj ?(info="") proc_proof sorts params context = function
    | C.AConstant (_, _, s, None, t, [], attrs)           ->
       [T.Statement (`Axiom, Some s, t, None, "")]
    | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
-      [T.Inductive (types, lpsno, "")] 
+      begin match is_record attrs with
+         | None    -> [T.Inductive (types, lpsno, "")]
+        | Some fs -> [T.Record (types, lpsno, fs, "")]
+      end
    | _                                          ->
       failwith "not a theorem, definition, axiom or inductive type"
 
@@ -134,3 +142,8 @@ let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
    in
    HLog.debug "Procedural: grafite rendering";
    List.rev (T.render_steps [] steps)
+
+let rec is_debug n = function
+   | []                   -> false
+   | G.IPDebug debug :: _ -> n <= debug
+   | _ :: tl              -> is_debug n tl