Records are now interpreted in the NG (but I am sure there is some bug

somewhere).

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 216b88b05ee69d3f4126f442a535c2562f54207a..5a22a4b62817c6cf354d9bcfa7668aa03deacff7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -794,8 +794,10 @@ EXTEND
         indty = tactic_term; paramspec = inverter_param_list ->
           G.Inverter
             (loc, name, indty, paramspec)
-            | IDENT "record" ; (params,name,ty,fields) = record_spec ->
+    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.Obj (loc, N.Record (params,name,ty,fields))
+    | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+        G.NObj (loc, N.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         G.Default (loc,what,uris)

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index e3384407cc06a0d1612f6baac12f59223952b69b..520db6aca994a6710ba955362387803e8564d7a7 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -27,6 +27,12 @@ let cic_name_of_name = function
   | _ -> assert false
 ;;
 
+let rec mk_rels howmany from =
+  match howmany with 
+  | 0 -> []
+  | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
+;;
+
 let refine_term 
  metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
   assert (uri=None);
@@ -539,51 +545,59 @@ let interpretate_obj
      let attrs = `Provided, `Regular in
      uri, height, [], [], 
      NCic.Inductive (true,leftno,tyl,attrs)
- | _ -> assert false
-(*
-  | CicNotationPt.Record (params,name,ty,fields) ->
-     let uri = match uri with Some uri -> uri | None -> assert false in
-     let context,params =
-      let context,res =
-       List.fold_left
-        (fun (context,res) (name,t) ->
-          let t =
-           match t with
-              None -> CicNotationPt.Implicit
-            | Some t -> t in
-          let name = cic_name_of_name name in
-           name::context,(name, interpretate_term context env None false t)::res
-        ) ([],[]) params
-      in
-       context,List.rev res in
-     let add_params =
-      List.fold_right
-       (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
-     let ty' = add_params (interpretate_term context env None false ty) in
-     let fields' =
-      snd (
-       List.fold_left
-        (fun (context,res) (name,ty,_coercion,arity) ->
-          let context' = Cic.Name name :: context in
-           context',(name,interpretate_term context env None false ty)::res
-        ) (context,[]) fields) in
-     let concl =
-      (*here the explicit_named_substituion is assumed to be of length 0 *)
-      let mutind = Cic.MutInd (uri,0,[]) in
-      if params = [] then mutind
-      else
-       Cic.Appl
-        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
-     let con =
+ | CicNotationPt.Record (params,name,ty,fields) ->
+    let context,params =
+     let context,res =
       List.fold_left
-       (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
-       concl fields' in
-     let con' = add_params con in
-     let tyl = [name,true,ty',["mk_" ^ name,con']] in
-     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
-      Cic.InductiveDefinition
-       (tyl,[],List.length params,[`Class (`Record field_names)])
-*)
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
+         in
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
+     in
+      context,List.rev res in
+    let add_params =
+     List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
+    let leftno = List.length params in
+    let ty' =
+     add_params
+      (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+        ~is_path:false ty) in
+    let fields' =
+     snd (
+      List.fold_left
+       (fun (context,res) (name,ty,_coercion,_arity) ->
+         let ty =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false ty in
+         let context' = (name,NCic.Decl ty)::context in
+          context',(name,ty)::res
+       ) (context,[]) fields) in
+    let concl =
+     let nref =
+      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+     let mutind = NCic.Const nref in
+     if params = [] then mutind
+     else
+      NCic.Appl
+       (mutind::mk_rels (List.length params) (List.length fields)) in
+    let con =
+     List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
+    let con' = add_params con in
+    let relevance = [] in
+    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
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty

diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index 86226fb02204aaf3110869b082c4946aa8d36108..75d3eda6a78bff973519efcc4b0659d341f026df 100644 (file)
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -42,4 +42,11 @@ nqed.
 (*
 ninductive nnat: Type ≝
    nO: nnat
- | nS: nnat → nnat. *)
\ No newline at end of file
+ | nS: nnat → nnat.
+*)
+
+(* testare anche i record e le ricorsioni/coricorsioni/(co)induttivi MUTUI *)
+
+(*
+nrecord pair: Type ≝ { l: pair; r: pair }.
+*)
\ No newline at end of file