X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_textual_parser%2FcicTextualParser.mly;h=9fd6ec52a1ec62c9c24991bc1f91f1a4ebc337ea;hb=a9e833b37216b225262450fd4e3fa5bf79ae4c3a;hp=3f6afc79a4685838fd9bb90a3f3990fe98119c5b;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 3f6afc79a..9fd6ec52a 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -30,8 +30,19 @@
  exception InvalidSuffix of string;;
  exception InductiveTypeURIExpected;;
  exception UnknownIdentifier of string;;
+ exception ExplicitNamedSubstitutionAppliedToRel;;
+ exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
  
- let uri_of_id_map = Hashtbl.create 53;;
+ (* merge removing duplicates of two lists free of duplicates *)
+ let union dom1 dom2 =
+  let rec filter =
+   function
+      [] -> []
+    | he::tl ->
+       if List.mem he dom1 then filter tl else he::(filter tl)
+  in
+   dom1 @ (filter dom2)
+ ;;
 
  let get_index_in_list e =
   let rec aux i =
@@ -41,17 +52,91 @@
     | _::tl -> aux (i+1) tl
   in
    aux 1
-;;
+ ;;
+
+ (* Returns the first meta whose number is above the *)
+ (* number of the higher meta.                       *)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let new_meta () =
+  let rec aux =
+   function
+      None,[] -> 1
+    | Some n,[] -> n
+    | None,(n,_,_)::tl -> aux (Some n,tl)
+    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+  in
+   1 + aux (None,!CicTextualParser0.metasenv)
+ ;;
+
+ (* identity_relocation_list_for_metavariable i canonical_context         *)
+ (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+ (* where n = List.length [canonical_context]                             *)
+ (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let identity_relocation_list_for_metavariable canonical_context =
+  let canonical_context_length = List.length canonical_context in
+   let rec aux =
+    function
+       (_,[]) -> []
+     | (n,None::tl) -> None::(aux ((n+1),tl))
+     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
+   in
+    aux (1,canonical_context)
+ ;;
+
+ let deoptionize_exp_named_subst =
+  function
+     None -> [], (function _ -> [])
+   | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
+ ;;
+
+ let term_of_con_uri uri exp_named_subst =
+  Const (uri,exp_named_subst)
+ ;;
+
+ let term_of_var_uri uri exp_named_subst =
+  Var (uri,exp_named_subst)
+ ;;
 
- let get_cookingno uri =
-  UriManager.relative_depth !CicTextualParser0.current_uri uri 0
+ let term_of_indty_uri (uri,tyno) exp_named_subst =
+  MutInd (uri, tyno, exp_named_subst)
+ ;;
+
+ let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
+  MutConstruct (uri, tyno, consno, exp_named_subst)
+ ;;
+
+ let term_of_uri uri =
+  match uri with
+     CicTextualParser0.ConUri uri ->
+      term_of_con_uri uri
+   | CicTextualParser0.VarUri uri ->
+      term_of_var_uri uri
+   | CicTextualParser0.IndTyUri (uri,tyno) ->
+      term_of_indty_uri (uri,tyno) 
+   | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+      term_of_indcon_uri (uri,tyno,consno)
+ ;;
+
+ let var_uri_of_id id interp =
+  match interp id with
+     None -> raise (UnknownIdentifier id)
+   | Some (CicTextualParser0.VarUri uri) -> uri
+   | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ ;;
+
+ let indty_uri_of_id id interp =
+  match interp id with
+     None -> raise (UnknownIdentifier id)
+   | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
+   | Some _ -> raise InductiveTypeURIExpected
  ;;
-  
 %}
 %token <string> ID
 %token <int> META
 %token <int> NUM
 %token <UriManager.uri> CONURI
+%token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
 %token ALIAS
@@ -59,197 +144,336 @@
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <Cic.term option> main
+%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
 %%
 main:
-   expr  { Some $1 }
- | alias { None }
- | EOF   { raise CicTextualParser0.Eof }
+ expr EOF { $1 }
 ;
 expr2:
-   CONURI
-   { let uri = UriManager.string_of_uri $1 in
-     let suff = (String.sub uri (String.length uri - 3) 3) in
-      match suff with
-         "con" ->
-           let cookingno = get_cookingno $1 in
-            Const ($1,cookingno)
-       | "var" -> Var $1
-       | _ -> raise (InvalidSuffix suff)
+   CONURI exp_named_subst
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
    }
- | INDTYURI
-    { let cookingno = get_cookingno (fst $1) in
-       MutInd (fst $1, cookingno, snd $1) }
- | INDCONURI
-   { let (uri,tyno,consno) = $1 in
-      let cookingno = get_cookingno uri in
-       MutConstruct (uri, cookingno, tyno, consno) }
- | ID
+ | VARURI exp_named_subst
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
+   }
+ | INDTYURI exp_named_subst
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
+   }
+ | INDCONURI exp_named_subst
+   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+      dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
+   }
+ | ID exp_named_subst
    { try
+      let res =
        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
+      in
+       (match $2 with
+           None -> ([], function _ -> res)
+         | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
+       )
      with
       Not_found ->
-       try
-        Hashtbl.find uri_of_id_map $1
-       with
-        Not_found ->
-         raise (UnknownIdentifier $1)
+       let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
+        let dom = union dom1 [$1] in
+         dom,
+          function interp ->
+           match interp $1 with
+	      None  -> raise (UnknownIdentifier $1)
+	    | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { let cookingno = get_cookingno (fst $5) in
-       MutCase (fst $5, cookingno, snd $5, $7, $3, $10) }
+    { let dom1,mk_expr1 = $3 in
+      let dom2,mk_expr2 = $7 in
+      let dom3,mk_expr3 = $10 in
+       let dom = union dom1 (union dom2 dom3) in
+        dom,
+        function interp ->
+         MutCase
+          (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
+    }
  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
-    { try
-       let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
-        raise InductiveTypeURIExpected
-      with
-       Not_found ->
-        match Hashtbl.find uri_of_id_map $5 with
-           MutInd (uri,cookingno,typeno) ->
-            MutCase (uri, cookingno, typeno, $7, $3, $10)
-         | _ -> raise InductiveTypeURIExpected
+    { let dom1,mk_expr1 = $3 in
+      let dom2,mk_expr2 = $7 in
+      let dom3,mk_expr3 = $10 in
+       let dom = union [$5] (union dom1 (union dom2 dom3)) in
+        dom,
+        function interp ->
+         let uri,typeno = indty_uri_of_id $5 interp in
+          MutCase
+           (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
+             (mk_expr3 interp))
     }
  | fixheader LCURLY exprseplist RCURLY
-    { let fixfunsdecls = snd $1 in
-      let fixfunsbodies = $3 in
-       let idx =
-        let rec find idx =
-         function
-            [] -> raise Not_found
-          | (name,_,_)::_  when name = (fst $1) -> idx
-          | _::tl -> find (idx+1) tl
-        in
-         find 0 fixfunsdecls
-       in
-        let fixfuns =
-         List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
-          fixfunsdecls fixfunsbodies
-        in
-         for i = 1 to List.length fixfuns do
-          CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-         done ;
-         Fix (idx,fixfuns)
+    { let dom1,mk_fixheader = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->
+          let fixfunsdecls = snd (mk_fixheader interp) in
+          let fixfunsbodies = (mk_exprseplist interp) in
+           let idx =
+            let rec find idx =
+             function
+                [] -> raise Not_found
+              | (name,_,_)::_  when name = (fst (mk_fixheader interp)) -> idx
+              | _::tl -> find (idx+1) tl
+            in
+             find 0 fixfunsdecls
+           in
+            let fixfuns =
+             List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
+              fixfunsdecls fixfunsbodies
+            in
+             for i = 1 to List.length fixfuns do
+              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+             done ;
+             Fix (idx,fixfuns)
     }
  | cofixheader LCURLY exprseplist RCURLY
-    { let cofixfunsdecls = (snd $1) in
-      let cofixfunsbodies = $3 in
-       let idx =
-        let rec find idx =
-         function
-            [] -> raise Not_found
-          | (name,_)::_  when name = (fst $1) -> idx
-          | _::tl -> find (idx+1) tl
-        in
-         find 0 cofixfunsdecls
-       in
-        let cofixfuns =
-         List.map2 (fun (name,ty) bo -> (name,ty,bo))
-          cofixfunsdecls cofixfunsbodies
+    { let dom1,mk_cofixheader = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->
+          let cofixfunsdecls = (snd (mk_cofixheader interp)) in
+          let cofixfunsbodies = mk_exprseplist interp in
+           let idx =
+            let rec find idx =
+             function
+                [] -> raise Not_found
+              | (name,_)::_  when name = (fst (mk_cofixheader interp)) -> idx
+              | _::tl -> find (idx+1) tl
+            in
+             find 0 cofixfunsdecls
+           in
+            let cofixfuns =
+             List.map2 (fun (name,ty) bo -> (name,ty,bo))
+              cofixfunsdecls cofixfunsbodies
+            in
+             for i = 1 to List.length cofixfuns do
+              CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+             done ;
+             CoFix (idx,cofixfuns)
+    }
+ | IMPLICIT
+    { let newmeta = new_meta () in
+       let new_canonical_context = [] in
+        let irl =
+         identity_relocation_list_for_metavariable new_canonical_context
         in
-         for i = 1 to List.length cofixfuns do
-          CicTextualParser0.binders := List.tl !CicTextualParser0.binders
-         done ;
-         CoFix (idx,cofixfuns)
-    }
- | IMPLICIT { Implicit }
- | SET { Sort Set }
- | PROP { Sort Prop }
- | TYPE { Sort Type }
- | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } 
- | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
+         CicTextualParser0.metasenv :=
+          [newmeta, new_canonical_context, Sort Type ;
+           newmeta+1, new_canonical_context, Meta (newmeta,irl);
+           newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+          ] @ !CicTextualParser0.metasenv ;
+         [], function _ -> Meta (newmeta+2,irl)
+    }
+ | SET  { [], function _ -> Sort Set }
+ | PROP { [], function _ -> Sort Prop }
+ | TYPE { [], function _ -> Sort Type }
+ | LPAREN expr CAST expr RPAREN
+    { let dom1,mk_expr1 = $2 in
+      let dom2,mk_expr2 = $4 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
+    }
+ | META LBRACKET substitutionlist RBRACKET
+    { let dom,mk_substitutionlist = $3 in
+       dom, function interp -> Meta ($1, mk_substitutionlist interp)
+    } 
+ | LPAREN expr expr exprlist RPAREN
+    { let dom1,mk_expr1 = $2 in
+      let dom2,mk_expr2 = $3 in
+      let dom3,mk_exprlist = $4 in
+       let dom = union dom1 (union dom2 dom3) in
+        dom,
+         function interp ->
+          Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
+    }
+;
+exp_named_subst :
+    { None }
+ | LCURLY named_substs RCURLY
+    { Some $2 }
+;
+named_substs :
+   VARURI LETIN expr2
+    { let dom,mk_expr = $3 in
+       dom, function interp -> [$1, mk_expr interp] }
+ | ID LETIN expr2
+    { let dom1,mk_expr = $3 in
+       let dom = union [$1] dom1 in
+        dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
+ | VARURI LETIN expr2 SEMICOLON named_substs
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_named_substs = $5 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
+    }
+ | ID LETIN expr2 SEMICOLON named_substs
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_named_substs = $5 in
+       let dom = union [$1] (union dom1 dom2) in
+        dom,
+         function interp ->
+          (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
+    }
 ;
 expr :
    pihead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      Prod (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | lambdahead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      Lambda (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | letinhead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
-      LetIn (fst $1, snd $1,$2) }
+      let dom1,mk_expr1 = snd $1 in
+      let dom2,mk_expr2 = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
+    }
  | expr2
     { $1 }
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
-       CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-       $2,$4
+    { let dom,mk_fixfunsdecl = $4 in
+       dom,
+        function interp ->
+         let bs =
+          List.rev_map
+           (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
+         in
+          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+          $2,(mk_fixfunsdecl interp)
     }
 ;
 fixfunsdecl:
    ID LPAREN NUM RPAREN COLON expr
-    { [$1,$3,$6] }
+    { let dom,mk_expr = $6 in
+       dom, function interp -> [$1,$3,mk_expr interp]
+    }
  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
-    { ($1,$3,$6)::$8 }
+    { let dom1,mk_expr = $6 in
+      let dom2,mk_fixfunsdecl = $8 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+    }
 ;
 cofixheader:
    COFIX ID LCURLY cofixfunsdecl RCURLY
-    { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
-       CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
-       $2,$4
+    { let dom,mk_cofixfunsdecl = $4 in
+       dom,
+        function interp ->
+         let bs =
+          List.rev_map
+           (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
+         in
+          CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+          $2,(mk_cofixfunsdecl interp)
     }
 ;
 cofixfunsdecl:
    ID COLON expr
-    { [$1,$3] }
+    { let dom,mk_expr = $3 in
+       dom, function interp -> [$1,(mk_expr interp)]
+    }
  | ID COLON expr SEMICOLON cofixfunsdecl
-    { ($1,$3)::$5 }
+    { let dom1,mk_expr = $3 in
+      let dom2,mk_cofixfunsdecl = $5 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+    }
 ;
 pihead:
    PROD ID COLON expr DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
-      (Cic.Name $2, $4) }
+      let dom,mk_expr = $4 in
+       Cic.Name $2, (dom, function interp -> mk_expr interp)
+    }
  | expr2 ARROW
-   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
-     (Anonimous, $1) }
+   { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
+     let dom,mk_expr = $1 in
+      Anonymous, (dom, function interp -> mk_expr interp)
+   }
  | LPAREN expr RPAREN ARROW
-   { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
-     (Anonimous, $2) }
+   { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
+     let dom,mk_expr = $2 in
+      Anonymous, (dom, function interp -> mk_expr interp)
+   }
 ;
 lambdahead:
   LAMBDA ID COLON expr DOT
    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     (Cic.Name $2, $4) }
+     let dom,mk_expr = $4 in
+      Cic.Name $2, (dom, function interp -> mk_expr interp)
+   }
 ;
 letinhead:
   LAMBDA ID LETIN expr DOT
    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
-     (Cic.Name $2, $4) }
+     let dom,mk_expr = $4 in
+      Cic.Name $2, (dom, function interp -> mk_expr interp)
+   }
 ;
 branches:
-                            { [] }
- | expr SEMICOLON branches  { $1::$3 }
- | expr                     { [$1] }
+    { [], function _ -> [] }
+ | expr SEMICOLON branches
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_branches = $3 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_branches interp)
+    }
+ | expr
+    { let dom,mk_expr = $1 in
+       dom, function interp -> [mk_expr interp]
+    }
 ;
 exprlist:
-                  { [] }
- | expr exprlist  { $1::$2 }
+    
+    { [], function _ -> [] }
+ | expr exprlist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_exprlist = $2 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+    }
 ;
 exprseplist:
-   expr                        { [$1] }
- | expr SEMICOLON exprseplist  { $1::$3 }
+   expr
+    { let dom,mk_expr = $1 in
+       dom, function interp -> [mk_expr interp]
+    }
+ | expr SEMICOLON exprseplist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_exprseplist = $3 in
+       let dom = union dom1 dom2 in
+        dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
+    }
 ;
 substitutionlist:
-                                     { [] }
- | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
- | NONE SEMICOLON substitutionlist   { None::$3 }
-;
-alias:
-   ALIAS ID CONURI
-    { let cookingno = get_cookingno $3 in
-       Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) }
- | ALIAS ID INDTYURI
-    { let cookingno = get_cookingno (fst $3) in
-       Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) }
- | ALIAS ID INDCONURI
-    { let uri,indno,consno = $3 in
-       let cookingno = get_cookingno uri in
-        Hashtbl.add uri_of_id_map $2
-         (Cic.MutConstruct (uri, cookingno, indno ,consno))
+    { [], function _ -> [] }
+ | expr SEMICOLON substitutionlist
+    { let dom1,mk_expr = $1 in
+      let dom2,mk_substitutionlist = $3 in
+       let dom = union dom1 dom2 in
+        dom,
+         function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
+    }
+ | NONE SEMICOLON substitutionlist
+    { let dom,mk_exprsubstitutionlist = $3 in
+       dom, function interp -> None::(mk_exprsubstitutionlist interp)
     }
-
-
-