- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 62d05509c2084a0f7175f39cd11969670e58780c..5c0d0a7d5db30840ad39521f9f98df73a27a5d7d 100644 (file)
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -308,7 +308,6 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
-    | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | NotationPt.Ident _
     | NotationPt.Uri _
     | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
@@ -435,48 +434,12 @@ let interpretate_obj status
       | None,_ ->
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
-        (match bo with
-         | NotationPt.LetRec (kind, defs, _) ->
-             let inductive = kind = `Inductive in
-             let _,obj_context =
-               List.fold_left
-                 (fun (i,acc) (_,(name,_),_,k) -> 
-                  (i+1, 
-                    (ncic_name_of_ident name, NReference.reference_of_spec uri 
-                     (if inductive then NReference.Fix (i,k,0)
-                      else NReference.CoFix i)) :: acc))
-                 (0,[]) defs
-             in
-             let inductiveFuns =
-               List.map
-                 (fun (params, (name, typ), body, decr_idx) ->
-                   let add_binders kind t =
-                    List.fold_right
-                     (fun var t -> 
-                        NotationPt.Binder (kind, var, t)) params t
-                   in
-                   let cic_body =
-                     interpretate_term status
-                       ~obj_context ~context ~env ~uri:None ~is_path:false
-                       (add_binders `Lambda body) 
-                   in
-                   let cic_type =
-                     interpretate_term_option status
-                       ~obj_context:[]
-                       ~context ~env ~uri:None ~is_path:false `Type
-                       (HExtlib.map_option (add_binders `Pi) typ)
-                   in
-                   ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
-                 defs
-             in
-             NCic.Fixpoint (inductive,inductiveFuns,attrs)
-         | bo -> 
-             let bo = 
-               interpretate_term status
-                ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
-             in
-             NCic.Constant ([],name,Some bo,ty',attrs)))
- | NotationPt.Inductive (params,tyl) ->
+          let bo = 
+            interpretate_term status
+             ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+          in
+          NCic.Constant ([],name,Some bo,ty',attrs))
+ | NotationPt.Inductive (params,tyl,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -529,10 +492,10 @@ let interpretate_obj status
       ) tyl
     in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Regular in
+     let attrs = source, `Regular in
      uri, height, [], [], 
      NCic.Inductive (inductive,leftno,tyl,attrs)
- | NotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -583,9 +546,45 @@ let interpretate_obj status
     let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Record field_names in
+     let attrs = source, `Record field_names in
      uri, height, [], [], 
      NCic.Inductive (true,leftno,tyl,attrs)
+ | NotationPt.LetRec (kind, defs, attrs) ->
+     let inductive = kind = `Inductive in
+     let _,obj_context =
+       List.fold_left
+         (fun (i,acc) (_,(name,_),_,k) -> 
+          (i+1, 
+            (ncic_name_of_ident name, NReference.reference_of_spec uri 
+             (if inductive then NReference.Fix (i,k,0)
+              else NReference.CoFix i)) :: acc))
+         (0,[]) defs
+     in
+     let inductiveFuns =
+       List.map
+         (fun (params, (name, typ), body, decr_idx) ->
+           let add_binders kind t =
+            List.fold_right
+             (fun var t -> 
+                NotationPt.Binder (kind, var, t)) params t
+           in
+           let cic_body =
+             interpretate_term status
+               ~obj_context ~context ~env ~uri:None ~is_path:false
+               (add_binders `Lambda body) 
+           in
+           let cic_type =
+             interpretate_term_option status
+               ~obj_context:[]
+               ~context ~env ~uri:None ~is_path:false `Type
+               (HExtlib.map_option (add_binders `Pi) typ)
+           in
+           ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
+         defs
+     in
+     let height = (* XXX calculate *) 0 in
+     uri, height, [], [], 
+     NCic.Fixpoint (inductive,inductiveFuns,attrs)
 ;;
 
 let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst