parameter sintax added to axiom statement

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 6dee8f04066b2a1023cb006fad016f480b0a7719..72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
     in
      [B.H([],
-       (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+     (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+       (B.b_kw "by")::
        B.b_space::
        B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else
@@ -908,6 +909,7 @@ let recursion_kind2pres params kind =
         "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)"
   in
   B.b_h [] (B.b_kw kind :: params2pres params)
+;;
 
 let inductive2pres term2pres ind =
   let constructor2pres decl =
@@ -924,13 +926,95 @@ let inductive2pres term2pres ind =
       term2pres ind.Content.inductive_type ]
     :: List.map constructor2pres ind.Content.inductive_constructors)
 
-let joint_def2pres term2pres def =
+let definition2pres ?recno term2pres d =
+  let name = match d.Content.def_name with Some x -> x|_->assert false in
+  let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
+  let ty = d.Content.def_type in
+  let module P = CicNotationPt in
+  let rec split_pi i t = 
+    if i <= 1 then 
+      match t with 
+      | P.Binder ((`Pi|`Forall),(var,_ as v),t) 
+      | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) -> 
+            [v], var, t 
+      | _ -> assert false
+    else
+      match t with
+      | P.Binder ((`Pi|`Forall), var ,ty) 
+      | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) ->
+           let l, r, t = split_pi (i-1) ty in
+           var :: l, r, t
+      | _ -> assert false
+  in 
+  let params, rec_param, ty = split_pi rno ty in
+  let body = d.Content.def_term in
+  let params = 
+    List.map 
+      (function 
+      | (name,Some ty) -> 
+          B.b_h [] [B.b_text [] "("; term2pres name; B.b_text [] " : ";
+                    B.b_space; term2pres ty; B.b_text [] ")"; B.b_space]
+      | (name,None) -> B.b_h [] [term2pres name;B.b_space]) 
+      params
+  in
+  B.b_hv [] 
+   [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
+    ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @ 
+        [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])] 
+      @ [B.b_h [] 
+         ((if rno <> -1 then 
+           [B.b_kw "on";B.b_space;term2pres rec_param] else [])
+         @ [ B.b_space; B.b_text [] ":";]) ]
+      @[ B.indent(term2pres ty)]); 
+   B.b_text [] ":=";
+   B.b_h [] [B.b_space;term2pres body] ]
+;;
+
+let joint_def2pres ?recno term2pres def =
   match def with
   | `Inductive ind -> inductive2pres term2pres ind
-  | _ -> assert false (* ZACK or raise ToDo? *)
+  | _ -> assert false
+;;
+
+let njoint_def2pres ?recno term2pres def =
+  match def with
+  | `Inductive ind -> inductive2pres term2pres ind
+  | `Definition def -> definition2pres ?recno term2pres def 
+  | _ -> assert false
+;;
+
+let njoint_def2pres term2pres joint_kind defs =
+  match joint_kind with
+  | `Recursive recnos ->
+      B.b_hv [] (B.b_kw "nlet rec " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map2 (fun a b -> njoint_def2pres ~recno:a term2pres b) 
+            recnos defs)))
+  | `CoRecursive ->
+      B.b_hv [] (B.b_kw "nlet corec " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+  | `Inductive _ -> 
+      B.b_hv [] (B.b_kw "ninductive " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+  | `CoInductive _ -> 
+      B.b_hv [] (B.b_kw "ncoinductive " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+;;
 
 let content2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
   (id,params,metasenv,obj) 
 =
   match obj with
@@ -977,6 +1061,7 @@ let content2pres
   ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
 =
   content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
@@ -987,8 +1072,9 @@ let content2pres
           (TermContentPres.pp_ast ast)))
 
 let ncontent2pres0
-  ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
-  (id,params,metasenv,obj) 
+  ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+  (term2pres : ?prec:int -> 'a)
+  (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
@@ -1025,9 +1111,9 @@ let ncontent2pres0
           B.indent (term2pres decl.Content.dec_type)] @
           metasenv2pres term2pres metasenv)
   | `Joint joint ->
-      B.b_v []
-        (recursion_kind2pres params joint.Content.joint_kind
-        :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
+      B.b_v [] 
+        [njoint_def2pres term2pres 
+          joint.Content.joint_kind joint.Content.joint_defs]
   | _ -> raise ToDo
 
 let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =