- Makefile update

[helm.git] / matita / components / ng_kernel / nCicExtraction.ml

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 85054e84c827b62de42a997e2caade4f346a32f2..8b8a7b216c74e360238b183789ed2acdb3319c6c 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -76,7 +76,7 @@ type obj_kind =
  | TermDeclaration of term_former_decl
  | TermDefinition of term_former_def
  | LetRec of obj_kind list
- (* inductive and records missing *)
+ | Algebraic of (string * typ_context * (string * typ list) list) list
 
 type obj = NUri.uri * obj_kind
 
@@ -488,6 +488,26 @@ let obj_of_constant status ~metasenv uri height bo ty =
     | `Term _ -> assert false (* IMPOSSIBLE *)
 ;;
 
+let obj_of_inductive status ~metasenv uri ind leftno il =
+ let tyl =
+  HExtlib.filter_map
+   (fun _,name,arity,cl ->
+     match classify_not_term status true [] arity with
+      | `Proposition
+      | `KindOrType
+      | `Type -> assert false (* IMPOSSIBLE *)
+      | `PropKind -> None
+      | `Kind ->
+          let arity = kind_of status ~metasenv [] arity in
+          let ctx,_ as res = split_kind_prods [] arity in
+           Some (name,ctx,[])
+   ) il
+ in
+  match tyl with
+     [] -> status,None
+   | _ -> status, Some (uri, Algebraic tyl)
+;;
+
 let obj_of status (uri,height,metasenv,subst,obj_kind) =
  let obj_kind = apply_subst subst obj_kind in
  try
@@ -522,7 +542,8 @@ let obj_of status (uri,height,metasenv,subst,obj_kind) =
            fs (status,[])
       in
        status, Some (uri,LetRec objs)
-   | NCic.Inductive _ -> status,None (*CSC: TO BE IMPLEMENTED*)
+   | NCic.Inductive (ind,leftno,il,_) ->
+      obj_of_inductive status ~metasenv uri ind leftno il
  with
   NotInFOmega ->
    prerr_endline "-- NOT IN F_omega";
@@ -591,15 +612,43 @@ let rec pp_term status ctx =
  | LetIn (name,s,t) ->
     "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
     ")"
- | Match (ref,matched,pl) ->
+ | Match (r,matched,pl) ->
+    let constructors, leftno =
+     let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
+     let _,_,_,cl  = List.nth tys n in
+      cl,leftno
+    in
+    let rec eat_branch n ty pat =
+      match (ty, pat) with
+      | NCic.Prod (_, _, t), _ when n > 0 ->
+         eat_branch (pred n) t pat 
+      | NCic.Prod (_, _, t), Lambda (name, t') ->
+          (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
+          let cv, rhs = eat_branch 0 t t' in
+          name :: cv, rhs
+      | _, _ -> [], pat
+    in
+    let j = ref 0 in
+    let patterns =
+      try
+        List.map2
+          (fun (_, name, ty) pat ->
+            incr j;
+            name, eat_branch leftno ty pat
+          ) constructors pl
+      with Invalid_argument _ -> assert false
+    in
    "case " ^ pp_term status ctx matched ^ " of\n" ^
    String.concat "\n"
     (List.map
-      (fun p ->
-        (*CSC: BUG, TO BE IMPLEMENTED *)
-        let pattern,body = "???", pp_term status ctx p in
-        "  " ^ pattern ^ " -> " ^ body
-     ) pl)
+      (fun (name,(bound_names,rhs)) ->
+        let pattern,body =
+         (*CSC: BUG avoid name clashes *)
+         String.concat " " (String.capitalize name::bound_names),
+         pp_term status ((List.rev bound_names)@ctx) rhs
+        in
+         "  " ^ pattern ^ " -> " ^ body
+     ) patterns)
  | TLambda t -> pp_term status ctx t
  | Inst t -> pp_term status ctx t
 
@@ -635,11 +684,24 @@ let rec pp_obj status (uri,obj_kind) =
  | TermDefinition ((ctx,ty),bo) ->
     let name = name_of_uri `FunctionName uri in
     let namectx = namectx_of_ctx ctx in
+    (*CSC: BUG here *)
     name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^
     name ^ " = " ^ pp_term status namectx bo
  | LetRec l ->
     (*CSC: BUG always uses the name of the URI *)
     String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
+ | Algebraic il ->
+    String.concat "\n"
+     (List.map
+      (fun _name,ctx,cl ->
+        (*CSC: BUG always uses the name of the URI *)
+        "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
+        String.concat " | " (List.map
+         (fun name,tys ->
+          capitalize `Constructor name ^
+           String.concat " " (List.map (pp_typ status []) tys)
+         ) cl
+      )) il)
  (* inductive and records missing *)
 
 let haskell_of_obj status obj =